Left Termination of the query pattern
qs(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 187 ms)
↳2 TRIPLES
↳3 UndefinedPredicateInTriplesTransformerProof (⇒, 0 ms)
↳4 TRIPLES
↳5 TriplesToPiDPProof (⇒, 499 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
    ↳9 PiDP
        ↳10 UsableRulesProof (⇔, 0 ms)
        ↳11 PiDP
        ↳12 PiDPToQDPProof (⇒, 11 ms)
        ↳13 QDP
        ↳14 QDPSizeChangeProof (⇔, 0 ms)
        ↳15 YES
    ↳16 PiDP
        ↳17 UsableRulesProof (⇔, 0 ms)
        ↳18 PiDP
        ↳19 PiDPToQDPProof (⇒, 0 ms)
        ↳20 QDP
        ↳21 QDPSizeChangeProof (⇔, 0 ms)
        ↳22 YES
    ↳23 PiDP
        ↳24 UsableRulesProof (⇔, 0 ms)
        ↳25 PiDP
        ↳26 PiDPToQDPProof (⇔, 0 ms)
        ↳27 QDP
        ↳28 QDPSizeChangeProof (⇔, 0 ms)
        ↳29 YES
    ↳30 PiDP
        ↳31 UsableRulesProof (⇔, 0 ms)
        ↳32 PiDP
        ↳33 PiDPToQDPProof (⇒, 0 ms)
        ↳34 QDP
        ↳35 QDPSizeChangeProof (⇔, 0 ms)
        ↳36 YES
    ↳37 PiDP
        ↳38 UsableRulesProof (⇔, 0 ms)
        ↳39 PiDP
        ↳40 PiDPToQDPProof (⇒, 0 ms)
        ↳41 QDP
        ↳42 QDPOrderProof (⇔, 180 ms)
        ↳43 QDP
        ↳44 DependencyGraphProof (⇔, 0 ms)
        ↳45 TRUE
    ↳46 PiDP
        ↳47 UsableRulesProof (⇔, 0 ms)
        ↳48 PiDP
        ↳49 PiDPToQDPProof (⇒, 0 ms)
        ↳50 QDP
        ↳51 QDPOrderProof (⇔, 225 ms)
        ↳52 QDP
        ↳53 DependencyGraphProof (⇔, 0 ms)
        ↳54 TRUE

(0) Obligation:

Clauses:

qs([], []).
qs(.(X, Xs), Ys) :- ','(part(X, Xs, Littles, Bigs), ','(qs(Littles, Ls), ','(qs(Bigs, Bs), app(Ls, .(X, Bs), Ys)))).
part(X, .(Y, Xs), .(Y, Ls), Bs) :- ','(less(X, Y), part(X, Xs, Ls, Bs)).
part(X, .(Y, Xs), Ls, .(Y, Bs)) :- part(X, Xs, Ls, Bs).
part(X1, [], [], []).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).
less(0, s(X2)).
less(s(X), s(Y)) :- less(X, Y).

Query: qs(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

lessA(s(X1), s(X2)) :- lessA(X1, X2).
partB(X1, .(X2, X3), .(X2, X4), X5) :- lessA(X1, X2).
partB(X1, .(X2, X3), .(X2, X4), X5) :- ','(lesscA(X1, X2), partB(X1, X3, X4, X5)).
partB(X1, .(X2, X3), X4, .(X2, X5)) :- partB(X1, X3, X4, X5).
qsE(.(X1, X2), X3) :- partB(X1, X2, X4, X5).
qsE(.(X1, X2), X3) :- ','(partcB(X1, X2, X4, X5), qsE(X4, X6)).
qsE(.(X1, X2), X3) :- ','(partcB(X1, X2, X4, X5), ','(qscE(X4, X6), qsE(X5, X7))).
qsE(.(X1, X2), X3) :- ','(partcB(X1, X2, X4, X5), ','(qscE(X4, X6), ','(qscE(X5, X7), appH(X6, X1, X7, X3)))).
appH(.(X1, X2), X3, X4, .(X1, X5)) :- appH(X2, X3, X4, X5).
appF(.(X1, X2), X3, X4, .(X1, X5)) :- appF(X2, X3, X4, X5).
pD(X1, X2, X3, X4, X5) :- qsE(X1, X2).
pD(X1, X2, X3, X4, X5) :- ','(qscE(X1, X2), appF(X3, X4, X2, X5)).
qsC(.(X1, .(X2, X3)), X4) :- lessA(X1, X2).
qsC(.(X1, .(X2, X3)), X4) :- ','(lesscA(X1, X2), partB(X1, X3, X5, X6)).
qsC(.(X1, .(X2, X3)), X4) :- ','(lesscA(X1, X2), ','(partcB(X1, X3, X5, X6), qsC(.(X2, X5), X7))).
qsC(.(X1, .(X2, X3)), X4) :- ','(lesscA(X1, X2), ','(partcB(X1, X3, X5, X6), ','(qscC(.(X2, X5), X7), pD(X6, X8, X7, X1, X4)))).
qsC(.(X1, .(X2, X3)), X4) :- partB(X1, X3, X5, X6).
qsC(.(X1, .(X2, X3)), X4) :- ','(partcB(X1, X3, X5, X6), qsE(X5, X7)).
qsC(.(X1, .(X2, X3)), X4) :- ','(partcB(X1, X3, X5, X6), ','(qscE(X5, X7), pD(.(X2, X6), X8, X7, X1, X4))).
qsC(.(X1, []), X2) :- qsG(X3).
qsC(.(X1, []), X2) :- ','(qscG(X3), qsG(X4)).
qsC(.(X1, []), X2) :- ','(qscG(X3), ','(qscG(X4), appF(X3, X1, X4, X2))).

Clauses:

lesscA(0, s(X1)).
lesscA(s(X1), s(X2)) :- lesscA(X1, X2).
partcB(X1, .(X2, X3), .(X2, X4), X5) :- ','(lesscA(X1, X2), partcB(X1, X3, X4, X5)).
partcB(X1, .(X2, X3), X4, .(X2, X5)) :- partcB(X1, X3, X4, X5).
partcB(X1, [], [], []).
qscC([], []).
qscC(.(X1, .(X2, X3)), X4) :- ','(lesscA(X1, X2), ','(partcB(X1, X3, X5, X6), ','(qscC(.(X2, X5), X7), qcD(X6, X8, X7, X1, X4)))).
qscC(.(X1, .(X2, X3)), X4) :- ','(partcB(X1, X3, X5, X6), ','(qscE(X5, X7), qcD(.(X2, X6), X8, X7, X1, X4))).
qscC(.(X1, []), X2) :- ','(qscG(X3), ','(qscG(X4), appcF(X3, X1, X4, X2))).
qscE([], []).
qscE(.(X1, X2), X3) :- ','(partcB(X1, X2, X4, X5), ','(qscE(X4, X6), ','(qscE(X5, X7), appcH(X6, X1, X7, X3)))).
appcH([], X1, X2, .(X1, X2)).
appcH(.(X1, X2), X3, X4, .(X1, X5)) :- appcH(X2, X3, X4, X5).
appcF([], X1, X2, .(X1, X2)).
appcF(.(X1, X2), X3, X4, .(X1, X5)) :- appcF(X2, X3, X4, X5).
qcD(X1, X2, X3, X4, X5) :- ','(qscE(X1, X2), appcF(X3, X4, X2, X5)).
qscG([]).

Afs:

qsC(x1, x2)  =  qsC(x1)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [DT09].

(4) Obligation:

Triples:

lessA(s(X1), s(X2)) :- lessA(X1, X2).
partB(X1, .(X2, X3), .(X2, X4), X5) :- lessA(X1, X2).
partB(X1, .(X2, X3), .(X2, X4), X5) :- ','(lesscA(X1, X2), partB(X1, X3, X4, X5)).
partB(X1, .(X2, X3), X4, .(X2, X5)) :- partB(X1, X3, X4, X5).
qsE(.(X1, X2), X3) :- partB(X1, X2, X4, X5).
qsE(.(X1, X2), X3) :- ','(partcB(X1, X2, X4, X5), qsE(X4, X6)).
qsE(.(X1, X2), X3) :- ','(partcB(X1, X2, X4, X5), ','(qscE(X4, X6), qsE(X5, X7))).
qsE(.(X1, X2), X3) :- ','(partcB(X1, X2, X4, X5), ','(qscE(X4, X6), ','(qscE(X5, X7), appH(X6, X1, X7, X3)))).
appH(.(X1, X2), X3, X4, .(X1, X5)) :- appH(X2, X3, X4, X5).
appF(.(X1, X2), X3, X4, .(X1, X5)) :- appF(X2, X3, X4, X5).
pD(X1, X2, X3, X4, X5) :- qsE(X1, X2).
pD(X1, X2, X3, X4, X5) :- ','(qscE(X1, X2), appF(X3, X4, X2, X5)).
qsC(.(X1, .(X2, X3)), X4) :- lessA(X1, X2).
qsC(.(X1, .(X2, X3)), X4) :- ','(lesscA(X1, X2), partB(X1, X3, X5, X6)).
qsC(.(X1, .(X2, X3)), X4) :- ','(lesscA(X1, X2), ','(partcB(X1, X3, X5, X6), qsC(.(X2, X5), X7))).
qsC(.(X1, .(X2, X3)), X4) :- ','(lesscA(X1, X2), ','(partcB(X1, X3, X5, X6), ','(qscC(.(X2, X5), X7), pD(X6, X8, X7, X1, X4)))).
qsC(.(X1, .(X2, X3)), X4) :- partB(X1, X3, X5, X6).
qsC(.(X1, .(X2, X3)), X4) :- ','(partcB(X1, X3, X5, X6), qsE(X5, X7)).
qsC(.(X1, .(X2, X3)), X4) :- ','(partcB(X1, X3, X5, X6), ','(qscE(X5, X7), pD(.(X2, X6), X8, X7, X1, X4))).
qsC(.(X1, []), X2) :- ','(qscG(X3), ','(qscG(X4), appF(X3, X1, X4, X2))).

Clauses:

lesscA(0, s(X1)).
lesscA(s(X1), s(X2)) :- lesscA(X1, X2).
partcB(X1, .(X2, X3), .(X2, X4), X5) :- ','(lesscA(X1, X2), partcB(X1, X3, X4, X5)).
partcB(X1, .(X2, X3), X4, .(X2, X5)) :- partcB(X1, X3, X4, X5).
partcB(X1, [], [], []).
qscC([], []).
qscC(.(X1, .(X2, X3)), X4) :- ','(lesscA(X1, X2), ','(partcB(X1, X3, X5, X6), ','(qscC(.(X2, X5), X7), qcD(X6, X8, X7, X1, X4)))).
qscC(.(X1, .(X2, X3)), X4) :- ','(partcB(X1, X3, X5, X6), ','(qscE(X5, X7), qcD(.(X2, X6), X8, X7, X1, X4))).
qscC(.(X1, []), X2) :- ','(qscG(X3), ','(qscG(X4), appcF(X3, X1, X4, X2))).
qscE([], []).
qscE(.(X1, X2), X3) :- ','(partcB(X1, X2, X4, X5), ','(qscE(X4, X6), ','(qscE(X5, X7), appcH(X6, X1, X7, X3)))).
appcH([], X1, X2, .(X1, X2)).
appcH(.(X1, X2), X3, X4, .(X1, X5)) :- appcH(X2, X3, X4, X5).
appcF([], X1, X2, .(X1, X2)).
appcF(.(X1, X2), X3, X4, .(X1, X5)) :- appcF(X2, X3, X4, X5).
qcD(X1, X2, X3, X4, X5) :- ','(qscE(X1, X2), appcF(X3, X4, X2, X5)).
qscG([]).

Afs:

qsC(x1, x2)  =  qsC(x1)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
qsC_in: (b,f)
lessA_in: (b,b)
lesscA_in: (b,b)
partB_in: (b,b,f,f)
partcB_in: (b,b,f,f)
qsE_in: (b,f)
qscE_in: (b,f)
appcH_in: (b,b,b,f)
appH_in: (b,b,b,f)
pD_in: (b,f,b,b,f)
appF_in: (b,b,b,f)
qscC_in: (b,f)
qcD_in: (b,f,b,b,f)
appcF_in: (b,b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

QSC_IN_GA(.(X1, .(X2, X3)), X4) → U18_GA(X1, X2, X3, X4, lessA_in_gg(X1, X2))
QSC_IN_GA(.(X1, .(X2, X3)), X4) → LESSA_IN_GG(X1, X2)
LESSA_IN_GG(s(X1), s(X2)) → U1_GG(X1, X2, lessA_in_gg(X1, X2))
LESSA_IN_GG(s(X1), s(X2)) → LESSA_IN_GG(X1, X2)
QSC_IN_GA(.(X1, .(X2, X3)), X4) → U19_GA(X1, X2, X3, X4, lesscA_in_gg(X1, X2))
U19_GA(X1, X2, X3, X4, lesscA_out_gg(X1, X2)) → U20_GA(X1, X2, X3, X4, partB_in_ggaa(X1, X3, X5, X6))
U19_GA(X1, X2, X3, X4, lesscA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X5, X6)
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → U2_GGAA(X1, X2, X3, X4, X5, lessA_in_gg(X1, X2))
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → LESSA_IN_GG(X1, X2)
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → U3_GGAA(X1, X2, X3, X4, X5, lesscA_in_gg(X1, X2))
U3_GGAA(X1, X2, X3, X4, X5, lesscA_out_gg(X1, X2)) → U4_GGAA(X1, X2, X3, X4, X5, partB_in_ggaa(X1, X3, X4, X5))
U3_GGAA(X1, X2, X3, X4, X5, lesscA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → U5_GGAA(X1, X2, X3, X4, X5, partB_in_ggaa(X1, X3, X4, X5))
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → PARTB_IN_GGAA(X1, X3, X4, X5)
U19_GA(X1, X2, X3, X4, lesscA_out_gg(X1, X2)) → U21_GA(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U21_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U22_GA(X1, X2, X3, X4, qsC_in_ga(.(X2, X5), X7))
U21_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → QSC_IN_GA(.(X2, X5), X7)
QSC_IN_GA(.(X1, .(X2, X3)), X4) → U25_GA(X1, X2, X3, X4, partB_in_ggaa(X1, X3, X5, X6))
QSC_IN_GA(.(X1, .(X2, X3)), X4) → PARTB_IN_GGAA(X1, X3, X5, X6)
QSC_IN_GA(.(X1, .(X2, X3)), X4) → U26_GA(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U26_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U27_GA(X1, X2, X3, X4, qsE_in_ga(X5, X7))
U26_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → QSE_IN_GA(X5, X7)
QSE_IN_GA(.(X1, X2), X3) → U6_GA(X1, X2, X3, partB_in_ggaa(X1, X2, X4, X5))
QSE_IN_GA(.(X1, X2), X3) → PARTB_IN_GGAA(X1, X2, X4, X5)
QSE_IN_GA(.(X1, X2), X3) → U7_GA(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U7_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U8_GA(X1, X2, X3, qsE_in_ga(X4, X6))
U7_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → QSE_IN_GA(X4, X6)
U7_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U9_GA(X1, X2, X3, X5, qscE_in_ga(X4, X6))
U9_GA(X1, X2, X3, X5, qscE_out_ga(X4, X6)) → U10_GA(X1, X2, X3, qsE_in_ga(X5, X7))
U9_GA(X1, X2, X3, X5, qscE_out_ga(X4, X6)) → QSE_IN_GA(X5, X7)
U9_GA(X1, X2, X3, X5, qscE_out_ga(X4, X6)) → U11_GA(X1, X2, X3, X6, qscE_in_ga(X5, X7))
U11_GA(X1, X2, X3, X6, qscE_out_ga(X5, X7)) → U12_GA(X1, X2, X3, appH_in_ggga(X6, X1, X7, X3))
U11_GA(X1, X2, X3, X6, qscE_out_ga(X5, X7)) → APPH_IN_GGGA(X6, X1, X7, X3)
APPH_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U13_GGGA(X1, X2, X3, X4, X5, appH_in_ggga(X2, X3, X4, X5))
APPH_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPH_IN_GGGA(X2, X3, X4, X5)
U26_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U28_GA(X1, X2, X3, X4, X6, qscE_in_ga(X5, X7))
U28_GA(X1, X2, X3, X4, X6, qscE_out_ga(X5, X7)) → U29_GA(X1, X2, X3, X4, pD_in_gagga(.(X2, X6), X8, X7, X1, X4))
U28_GA(X1, X2, X3, X4, X6, qscE_out_ga(X5, X7)) → PD_IN_GAGGA(.(X2, X6), X8, X7, X1, X4)
PD_IN_GAGGA(X1, X2, X3, X4, X5) → U15_GAGGA(X1, X2, X3, X4, X5, qsE_in_ga(X1, X2))
PD_IN_GAGGA(X1, X2, X3, X4, X5) → QSE_IN_GA(X1, X2)
PD_IN_GAGGA(X1, X2, X3, X4, X5) → U16_GAGGA(X1, X2, X3, X4, X5, qscE_in_ga(X1, X2))
U16_GAGGA(X1, X2, X3, X4, X5, qscE_out_ga(X1, X2)) → U17_GAGGA(X1, X2, X3, X4, X5, appF_in_ggga(X3, X4, X2, X5))
U16_GAGGA(X1, X2, X3, X4, X5, qscE_out_ga(X1, X2)) → APPF_IN_GGGA(X3, X4, X2, X5)
APPF_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U14_GGGA(X1, X2, X3, X4, X5, appF_in_ggga(X2, X3, X4, X5))
APPF_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPF_IN_GGGA(X2, X3, X4, X5)
QSC_IN_GA(.(X1, []), X2) → U30_GA(X1, X2, qscG_in_a(X3))
U30_GA(X1, X2, qscG_out_a(X3)) → U31_GA(X1, X2, X3, qscG_in_a(X4))
U31_GA(X1, X2, X3, qscG_out_a(X4)) → U32_GA(X1, X2, appF_in_ggga(X3, X1, X4, X2))
U31_GA(X1, X2, X3, qscG_out_a(X4)) → APPF_IN_GGGA(X3, X1, X4, X2)
U21_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U23_GA(X1, X2, X3, X4, X6, qscC_in_ga(.(X2, X5), X7))
U23_GA(X1, X2, X3, X4, X6, qscC_out_ga(.(X2, X5), X7)) → U24_GA(X1, X2, X3, X4, pD_in_gagga(X6, X8, X7, X1, X4))
U23_GA(X1, X2, X3, X4, X6, qscC_out_ga(.(X2, X5), X7)) → PD_IN_GAGGA(X6, X8, X7, X1, X4)

The TRS R consists of the following rules:

lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U34_gg(X1, X2, lesscA_in_gg(X1, X2))
U34_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U35_ggaa(X1, X2, X3, X4, X5, lesscA_in_gg(X1, X2))
U35_ggaa(X1, X2, X3, X4, X5, lesscA_out_gg(X1, X2)) → U36_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U37_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U37_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U36_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscE_in_ga([], []) → qscE_out_ga([], [])
qscE_in_ga(.(X1, X2), X3) → U48_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U48_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U49_ga(X1, X2, X3, X5, qscE_in_ga(X4, X6))
U49_ga(X1, X2, X3, X5, qscE_out_ga(X4, X6)) → U50_ga(X1, X2, X3, X6, qscE_in_ga(X5, X7))
U50_ga(X1, X2, X3, X6, qscE_out_ga(X5, X7)) → U51_ga(X1, X2, X3, appcH_in_ggga(X6, X1, X7, X3))
appcH_in_ggga([], X1, X2, .(X1, X2)) → appcH_out_ggga([], X1, X2, .(X1, X2))
appcH_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U52_ggga(X1, X2, X3, X4, X5, appcH_in_ggga(X2, X3, X4, X5))
U52_ggga(X1, X2, X3, X4, X5, appcH_out_ggga(X2, X3, X4, X5)) → appcH_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U51_ga(X1, X2, X3, appcH_out_ggga(X6, X1, X7, X3)) → qscE_out_ga(.(X1, X2), X3)
qscG_in_a([]) → qscG_out_a([])
qscC_in_ga([], []) → qscC_out_ga([], [])
qscC_in_ga(.(X1, .(X2, X3)), X4) → U38_ga(X1, X2, X3, X4, lesscA_in_gg(X1, X2))
U38_ga(X1, X2, X3, X4, lesscA_out_gg(X1, X2)) → U39_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U39_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U40_ga(X1, X2, X3, X4, X6, qscC_in_ga(.(X2, X5), X7))
qscC_in_ga(.(X1, .(X2, X3)), X4) → U42_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U42_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U43_ga(X1, X2, X3, X4, X6, qscE_in_ga(X5, X7))
U43_ga(X1, X2, X3, X4, X6, qscE_out_ga(X5, X7)) → U44_ga(X1, X2, X3, X4, qcD_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcD_in_gagga(X1, X2, X3, X4, X5) → U54_gagga(X1, X2, X3, X4, X5, qscE_in_ga(X1, X2))
U54_gagga(X1, X2, X3, X4, X5, qscE_out_ga(X1, X2)) → U55_gagga(X1, X2, X3, X4, X5, appcF_in_ggga(X3, X4, X2, X5))
appcF_in_ggga([], X1, X2, .(X1, X2)) → appcF_out_ggga([], X1, X2, .(X1, X2))
appcF_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U53_ggga(X1, X2, X3, X4, X5, appcF_in_ggga(X2, X3, X4, X5))
U53_ggga(X1, X2, X3, X4, X5, appcF_out_ggga(X2, X3, X4, X5)) → appcF_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U55_gagga(X1, X2, X3, X4, X5, appcF_out_ggga(X3, X4, X2, X5)) → qcD_out_gagga(X1, X2, X3, X4, X5)
U44_ga(X1, X2, X3, X4, qcD_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscC_out_ga(.(X1, .(X2, X3)), X4)
qscC_in_ga(.(X1, []), X2) → U45_ga(X1, X2, qscG_in_a(X3))
U45_ga(X1, X2, qscG_out_a(X3)) → U46_ga(X1, X2, X3, qscG_in_a(X4))
U46_ga(X1, X2, X3, qscG_out_a(X4)) → U47_ga(X1, X2, appcF_in_ggga(X3, X1, X4, X2))
U47_ga(X1, X2, appcF_out_ggga(X3, X1, X4, X2)) → qscC_out_ga(.(X1, []), X2)
U40_ga(X1, X2, X3, X4, X6, qscC_out_ga(.(X2, X5), X7)) → U41_ga(X1, X2, X3, X4, qcD_in_gagga(X6, X8, X7, X1, X4))
U41_ga(X1, X2, X3, X4, qcD_out_gagga(X6, X8, X7, X1, X4)) → qscC_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
qsC_in_ga(x1, x2)  =  qsC_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
lessA_in_gg(x1, x2)  =  lessA_in_gg(x1, x2)
s(x1)  =  s(x1)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
0  =  0
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U34_gg(x1, x2, x3)  =  U34_gg(x1, x2, x3)
partB_in_ggaa(x1, x2, x3, x4)  =  partB_in_ggaa(x1, x2)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U35_ggaa(x1, x2, x3, x4, x5, x6)  =  U35_ggaa(x1, x2, x3, x6)
U36_ggaa(x1, x2, x3, x4, x5, x6)  =  U36_ggaa(x1, x2, x3, x6)
U37_ggaa(x1, x2, x3, x4, x5, x6)  =  U37_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qsE_in_ga(x1, x2)  =  qsE_in_ga(x1)
qscE_in_ga(x1, x2)  =  qscE_in_ga(x1)
qscE_out_ga(x1, x2)  =  qscE_out_ga(x1, x2)
U48_ga(x1, x2, x3, x4)  =  U48_ga(x1, x2, x4)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x4, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x4, x5)
U51_ga(x1, x2, x3, x4)  =  U51_ga(x1, x2, x4)
appcH_in_ggga(x1, x2, x3, x4)  =  appcH_in_ggga(x1, x2, x3)
appcH_out_ggga(x1, x2, x3, x4)  =  appcH_out_ggga(x1, x2, x3, x4)
U52_ggga(x1, x2, x3, x4, x5, x6)  =  U52_ggga(x1, x2, x3, x4, x6)
appH_in_ggga(x1, x2, x3, x4)  =  appH_in_ggga(x1, x2, x3)
pD_in_gagga(x1, x2, x3, x4, x5)  =  pD_in_gagga(x1, x3, x4)
appF_in_ggga(x1, x2, x3, x4)  =  appF_in_ggga(x1, x2, x3)
qscG_in_a(x1)  =  qscG_in_a
qscG_out_a(x1)  =  qscG_out_a(x1)
qscC_in_ga(x1, x2)  =  qscC_in_ga(x1)
qscC_out_ga(x1, x2)  =  qscC_out_ga(x1, x2)
U38_ga(x1, x2, x3, x4, x5)  =  U38_ga(x1, x2, x3, x5)
U39_ga(x1, x2, x3, x4, x5)  =  U39_ga(x1, x2, x3, x5)
U40_ga(x1, x2, x3, x4, x5, x6)  =  U40_ga(x1, x2, x3, x5, x6)
U42_ga(x1, x2, x3, x4, x5)  =  U42_ga(x1, x2, x3, x5)
U43_ga(x1, x2, x3, x4, x5, x6)  =  U43_ga(x1, x2, x3, x5, x6)
U44_ga(x1, x2, x3, x4, x5)  =  U44_ga(x1, x2, x3, x5)
qcD_in_gagga(x1, x2, x3, x4, x5)  =  qcD_in_gagga(x1, x3, x4)
U54_gagga(x1, x2, x3, x4, x5, x6)  =  U54_gagga(x1, x3, x4, x6)
U55_gagga(x1, x2, x3, x4, x5, x6)  =  U55_gagga(x1, x2, x3, x4, x6)
appcF_in_ggga(x1, x2, x3, x4)  =  appcF_in_ggga(x1, x2, x3)
appcF_out_ggga(x1, x2, x3, x4)  =  appcF_out_ggga(x1, x2, x3, x4)
U53_ggga(x1, x2, x3, x4, x5, x6)  =  U53_ggga(x1, x2, x3, x4, x6)
qcD_out_gagga(x1, x2, x3, x4, x5)  =  qcD_out_gagga(x1, x2, x3, x4, x5)
U45_ga(x1, x2, x3)  =  U45_ga(x1, x3)
U46_ga(x1, x2, x3, x4)  =  U46_ga(x1, x3, x4)
U47_ga(x1, x2, x3)  =  U47_ga(x1, x3)
U41_ga(x1, x2, x3, x4, x5)  =  U41_ga(x1, x2, x3, x5)
QSC_IN_GA(x1, x2)  =  QSC_IN_GA(x1)
U18_GA(x1, x2, x3, x4, x5)  =  U18_GA(x1, x2, x3, x5)
LESSA_IN_GG(x1, x2)  =  LESSA_IN_GG(x1, x2)
U1_GG(x1, x2, x3)  =  U1_GG(x1, x2, x3)
U19_GA(x1, x2, x3, x4, x5)  =  U19_GA(x1, x2, x3, x5)
U20_GA(x1, x2, x3, x4, x5)  =  U20_GA(x1, x2, x3, x5)
PARTB_IN_GGAA(x1, x2, x3, x4)  =  PARTB_IN_GGAA(x1, x2)
U2_GGAA(x1, x2, x3, x4, x5, x6)  =  U2_GGAA(x1, x2, x3, x6)
U3_GGAA(x1, x2, x3, x4, x5, x6)  =  U3_GGAA(x1, x2, x3, x6)
U4_GGAA(x1, x2, x3, x4, x5, x6)  =  U4_GGAA(x1, x2, x3, x6)
U5_GGAA(x1, x2, x3, x4, x5, x6)  =  U5_GGAA(x1, x2, x3, x6)
U21_GA(x1, x2, x3, x4, x5)  =  U21_GA(x1, x2, x3, x5)
U22_GA(x1, x2, x3, x4, x5)  =  U22_GA(x1, x2, x3, x5)
U25_GA(x1, x2, x3, x4, x5)  =  U25_GA(x1, x2, x3, x5)
U26_GA(x1, x2, x3, x4, x5)  =  U26_GA(x1, x2, x3, x5)
U27_GA(x1, x2, x3, x4, x5)  =  U27_GA(x1, x2, x3, x5)
QSE_IN_GA(x1, x2)  =  QSE_IN_GA(x1)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x2, x4)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x2, x4)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x2, x4)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x4, x5)
U10_GA(x1, x2, x3, x4)  =  U10_GA(x1, x2, x4)
U11_GA(x1, x2, x3, x4, x5)  =  U11_GA(x1, x2, x4, x5)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x2, x4)
APPH_IN_GGGA(x1, x2, x3, x4)  =  APPH_IN_GGGA(x1, x2, x3)
U13_GGGA(x1, x2, x3, x4, x5, x6)  =  U13_GGGA(x1, x2, x3, x4, x6)
U28_GA(x1, x2, x3, x4, x5, x6)  =  U28_GA(x1, x2, x3, x5, x6)
U29_GA(x1, x2, x3, x4, x5)  =  U29_GA(x1, x2, x3, x5)
PD_IN_GAGGA(x1, x2, x3, x4, x5)  =  PD_IN_GAGGA(x1, x3, x4)
U15_GAGGA(x1, x2, x3, x4, x5, x6)  =  U15_GAGGA(x1, x3, x4, x6)
U16_GAGGA(x1, x2, x3, x4, x5, x6)  =  U16_GAGGA(x1, x3, x4, x6)
U17_GAGGA(x1, x2, x3, x4, x5, x6)  =  U17_GAGGA(x1, x3, x4, x6)
APPF_IN_GGGA(x1, x2, x3, x4)  =  APPF_IN_GGGA(x1, x2, x3)
U14_GGGA(x1, x2, x3, x4, x5, x6)  =  U14_GGGA(x1, x2, x3, x4, x6)
U30_GA(x1, x2, x3)  =  U30_GA(x1, x3)
U31_GA(x1, x2, x3, x4)  =  U31_GA(x1, x3, x4)
U32_GA(x1, x2, x3)  =  U32_GA(x1, x3)
U23_GA(x1, x2, x3, x4, x5, x6)  =  U23_GA(x1, x2, x3, x5, x6)
U24_GA(x1, x2, x3, x4, x5)  =  U24_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QSC_IN_GA(.(X1, .(X2, X3)), X4) → U18_GA(X1, X2, X3, X4, lessA_in_gg(X1, X2))
QSC_IN_GA(.(X1, .(X2, X3)), X4) → LESSA_IN_GG(X1, X2)
LESSA_IN_GG(s(X1), s(X2)) → U1_GG(X1, X2, lessA_in_gg(X1, X2))
LESSA_IN_GG(s(X1), s(X2)) → LESSA_IN_GG(X1, X2)
QSC_IN_GA(.(X1, .(X2, X3)), X4) → U19_GA(X1, X2, X3, X4, lesscA_in_gg(X1, X2))
U19_GA(X1, X2, X3, X4, lesscA_out_gg(X1, X2)) → U20_GA(X1, X2, X3, X4, partB_in_ggaa(X1, X3, X5, X6))
U19_GA(X1, X2, X3, X4, lesscA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X5, X6)
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → U2_GGAA(X1, X2, X3, X4, X5, lessA_in_gg(X1, X2))
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → LESSA_IN_GG(X1, X2)
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → U3_GGAA(X1, X2, X3, X4, X5, lesscA_in_gg(X1, X2))
U3_GGAA(X1, X2, X3, X4, X5, lesscA_out_gg(X1, X2)) → U4_GGAA(X1, X2, X3, X4, X5, partB_in_ggaa(X1, X3, X4, X5))
U3_GGAA(X1, X2, X3, X4, X5, lesscA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → U5_GGAA(X1, X2, X3, X4, X5, partB_in_ggaa(X1, X3, X4, X5))
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → PARTB_IN_GGAA(X1, X3, X4, X5)
U19_GA(X1, X2, X3, X4, lesscA_out_gg(X1, X2)) → U21_GA(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U21_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U22_GA(X1, X2, X3, X4, qsC_in_ga(.(X2, X5), X7))
U21_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → QSC_IN_GA(.(X2, X5), X7)
QSC_IN_GA(.(X1, .(X2, X3)), X4) → U25_GA(X1, X2, X3, X4, partB_in_ggaa(X1, X3, X5, X6))
QSC_IN_GA(.(X1, .(X2, X3)), X4) → PARTB_IN_GGAA(X1, X3, X5, X6)
QSC_IN_GA(.(X1, .(X2, X3)), X4) → U26_GA(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U26_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U27_GA(X1, X2, X3, X4, qsE_in_ga(X5, X7))
U26_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → QSE_IN_GA(X5, X7)
QSE_IN_GA(.(X1, X2), X3) → U6_GA(X1, X2, X3, partB_in_ggaa(X1, X2, X4, X5))
QSE_IN_GA(.(X1, X2), X3) → PARTB_IN_GGAA(X1, X2, X4, X5)
QSE_IN_GA(.(X1, X2), X3) → U7_GA(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U7_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U8_GA(X1, X2, X3, qsE_in_ga(X4, X6))
U7_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → QSE_IN_GA(X4, X6)
U7_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U9_GA(X1, X2, X3, X5, qscE_in_ga(X4, X6))
U9_GA(X1, X2, X3, X5, qscE_out_ga(X4, X6)) → U10_GA(X1, X2, X3, qsE_in_ga(X5, X7))
U9_GA(X1, X2, X3, X5, qscE_out_ga(X4, X6)) → QSE_IN_GA(X5, X7)
U9_GA(X1, X2, X3, X5, qscE_out_ga(X4, X6)) → U11_GA(X1, X2, X3, X6, qscE_in_ga(X5, X7))
U11_GA(X1, X2, X3, X6, qscE_out_ga(X5, X7)) → U12_GA(X1, X2, X3, appH_in_ggga(X6, X1, X7, X3))
U11_GA(X1, X2, X3, X6, qscE_out_ga(X5, X7)) → APPH_IN_GGGA(X6, X1, X7, X3)
APPH_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U13_GGGA(X1, X2, X3, X4, X5, appH_in_ggga(X2, X3, X4, X5))
APPH_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPH_IN_GGGA(X2, X3, X4, X5)
U26_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U28_GA(X1, X2, X3, X4, X6, qscE_in_ga(X5, X7))
U28_GA(X1, X2, X3, X4, X6, qscE_out_ga(X5, X7)) → U29_GA(X1, X2, X3, X4, pD_in_gagga(.(X2, X6), X8, X7, X1, X4))
U28_GA(X1, X2, X3, X4, X6, qscE_out_ga(X5, X7)) → PD_IN_GAGGA(.(X2, X6), X8, X7, X1, X4)
PD_IN_GAGGA(X1, X2, X3, X4, X5) → U15_GAGGA(X1, X2, X3, X4, X5, qsE_in_ga(X1, X2))
PD_IN_GAGGA(X1, X2, X3, X4, X5) → QSE_IN_GA(X1, X2)
PD_IN_GAGGA(X1, X2, X3, X4, X5) → U16_GAGGA(X1, X2, X3, X4, X5, qscE_in_ga(X1, X2))
U16_GAGGA(X1, X2, X3, X4, X5, qscE_out_ga(X1, X2)) → U17_GAGGA(X1, X2, X3, X4, X5, appF_in_ggga(X3, X4, X2, X5))
U16_GAGGA(X1, X2, X3, X4, X5, qscE_out_ga(X1, X2)) → APPF_IN_GGGA(X3, X4, X2, X5)
APPF_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U14_GGGA(X1, X2, X3, X4, X5, appF_in_ggga(X2, X3, X4, X5))
APPF_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPF_IN_GGGA(X2, X3, X4, X5)
QSC_IN_GA(.(X1, []), X2) → U30_GA(X1, X2, qscG_in_a(X3))
U30_GA(X1, X2, qscG_out_a(X3)) → U31_GA(X1, X2, X3, qscG_in_a(X4))
U31_GA(X1, X2, X3, qscG_out_a(X4)) → U32_GA(X1, X2, appF_in_ggga(X3, X1, X4, X2))
U31_GA(X1, X2, X3, qscG_out_a(X4)) → APPF_IN_GGGA(X3, X1, X4, X2)
U21_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U23_GA(X1, X2, X3, X4, X6, qscC_in_ga(.(X2, X5), X7))
U23_GA(X1, X2, X3, X4, X6, qscC_out_ga(.(X2, X5), X7)) → U24_GA(X1, X2, X3, X4, pD_in_gagga(X6, X8, X7, X1, X4))
U23_GA(X1, X2, X3, X4, X6, qscC_out_ga(.(X2, X5), X7)) → PD_IN_GAGGA(X6, X8, X7, X1, X4)

The TRS R consists of the following rules:

lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U34_gg(X1, X2, lesscA_in_gg(X1, X2))
U34_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U35_ggaa(X1, X2, X3, X4, X5, lesscA_in_gg(X1, X2))
U35_ggaa(X1, X2, X3, X4, X5, lesscA_out_gg(X1, X2)) → U36_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U37_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U37_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U36_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscE_in_ga([], []) → qscE_out_ga([], [])
qscE_in_ga(.(X1, X2), X3) → U48_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U48_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U49_ga(X1, X2, X3, X5, qscE_in_ga(X4, X6))
U49_ga(X1, X2, X3, X5, qscE_out_ga(X4, X6)) → U50_ga(X1, X2, X3, X6, qscE_in_ga(X5, X7))
U50_ga(X1, X2, X3, X6, qscE_out_ga(X5, X7)) → U51_ga(X1, X2, X3, appcH_in_ggga(X6, X1, X7, X3))
appcH_in_ggga([], X1, X2, .(X1, X2)) → appcH_out_ggga([], X1, X2, .(X1, X2))
appcH_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U52_ggga(X1, X2, X3, X4, X5, appcH_in_ggga(X2, X3, X4, X5))
U52_ggga(X1, X2, X3, X4, X5, appcH_out_ggga(X2, X3, X4, X5)) → appcH_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U51_ga(X1, X2, X3, appcH_out_ggga(X6, X1, X7, X3)) → qscE_out_ga(.(X1, X2), X3)
qscG_in_a([]) → qscG_out_a([])
qscC_in_ga([], []) → qscC_out_ga([], [])
qscC_in_ga(.(X1, .(X2, X3)), X4) → U38_ga(X1, X2, X3, X4, lesscA_in_gg(X1, X2))
U38_ga(X1, X2, X3, X4, lesscA_out_gg(X1, X2)) → U39_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U39_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U40_ga(X1, X2, X3, X4, X6, qscC_in_ga(.(X2, X5), X7))
qscC_in_ga(.(X1, .(X2, X3)), X4) → U42_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U42_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U43_ga(X1, X2, X3, X4, X6, qscE_in_ga(X5, X7))
U43_ga(X1, X2, X3, X4, X6, qscE_out_ga(X5, X7)) → U44_ga(X1, X2, X3, X4, qcD_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcD_in_gagga(X1, X2, X3, X4, X5) → U54_gagga(X1, X2, X3, X4, X5, qscE_in_ga(X1, X2))
U54_gagga(X1, X2, X3, X4, X5, qscE_out_ga(X1, X2)) → U55_gagga(X1, X2, X3, X4, X5, appcF_in_ggga(X3, X4, X2, X5))
appcF_in_ggga([], X1, X2, .(X1, X2)) → appcF_out_ggga([], X1, X2, .(X1, X2))
appcF_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U53_ggga(X1, X2, X3, X4, X5, appcF_in_ggga(X2, X3, X4, X5))
U53_ggga(X1, X2, X3, X4, X5, appcF_out_ggga(X2, X3, X4, X5)) → appcF_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U55_gagga(X1, X2, X3, X4, X5, appcF_out_ggga(X3, X4, X2, X5)) → qcD_out_gagga(X1, X2, X3, X4, X5)
U44_ga(X1, X2, X3, X4, qcD_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscC_out_ga(.(X1, .(X2, X3)), X4)
qscC_in_ga(.(X1, []), X2) → U45_ga(X1, X2, qscG_in_a(X3))
U45_ga(X1, X2, qscG_out_a(X3)) → U46_ga(X1, X2, X3, qscG_in_a(X4))
U46_ga(X1, X2, X3, qscG_out_a(X4)) → U47_ga(X1, X2, appcF_in_ggga(X3, X1, X4, X2))
U47_ga(X1, X2, appcF_out_ggga(X3, X1, X4, X2)) → qscC_out_ga(.(X1, []), X2)
U40_ga(X1, X2, X3, X4, X6, qscC_out_ga(.(X2, X5), X7)) → U41_ga(X1, X2, X3, X4, qcD_in_gagga(X6, X8, X7, X1, X4))
U41_ga(X1, X2, X3, X4, qcD_out_gagga(X6, X8, X7, X1, X4)) → qscC_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
qsC_in_ga(x1, x2)  =  qsC_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
lessA_in_gg(x1, x2)  =  lessA_in_gg(x1, x2)
s(x1)  =  s(x1)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
0  =  0
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U34_gg(x1, x2, x3)  =  U34_gg(x1, x2, x3)
partB_in_ggaa(x1, x2, x3, x4)  =  partB_in_ggaa(x1, x2)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U35_ggaa(x1, x2, x3, x4, x5, x6)  =  U35_ggaa(x1, x2, x3, x6)
U36_ggaa(x1, x2, x3, x4, x5, x6)  =  U36_ggaa(x1, x2, x3, x6)
U37_ggaa(x1, x2, x3, x4, x5, x6)  =  U37_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qsE_in_ga(x1, x2)  =  qsE_in_ga(x1)
qscE_in_ga(x1, x2)  =  qscE_in_ga(x1)
qscE_out_ga(x1, x2)  =  qscE_out_ga(x1, x2)
U48_ga(x1, x2, x3, x4)  =  U48_ga(x1, x2, x4)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x4, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x4, x5)
U51_ga(x1, x2, x3, x4)  =  U51_ga(x1, x2, x4)
appcH_in_ggga(x1, x2, x3, x4)  =  appcH_in_ggga(x1, x2, x3)
appcH_out_ggga(x1, x2, x3, x4)  =  appcH_out_ggga(x1, x2, x3, x4)
U52_ggga(x1, x2, x3, x4, x5, x6)  =  U52_ggga(x1, x2, x3, x4, x6)
appH_in_ggga(x1, x2, x3, x4)  =  appH_in_ggga(x1, x2, x3)
pD_in_gagga(x1, x2, x3, x4, x5)  =  pD_in_gagga(x1, x3, x4)
appF_in_ggga(x1, x2, x3, x4)  =  appF_in_ggga(x1, x2, x3)
qscG_in_a(x1)  =  qscG_in_a
qscG_out_a(x1)  =  qscG_out_a(x1)
qscC_in_ga(x1, x2)  =  qscC_in_ga(x1)
qscC_out_ga(x1, x2)  =  qscC_out_ga(x1, x2)
U38_ga(x1, x2, x3, x4, x5)  =  U38_ga(x1, x2, x3, x5)
U39_ga(x1, x2, x3, x4, x5)  =  U39_ga(x1, x2, x3, x5)
U40_ga(x1, x2, x3, x4, x5, x6)  =  U40_ga(x1, x2, x3, x5, x6)
U42_ga(x1, x2, x3, x4, x5)  =  U42_ga(x1, x2, x3, x5)
U43_ga(x1, x2, x3, x4, x5, x6)  =  U43_ga(x1, x2, x3, x5, x6)
U44_ga(x1, x2, x3, x4, x5)  =  U44_ga(x1, x2, x3, x5)
qcD_in_gagga(x1, x2, x3, x4, x5)  =  qcD_in_gagga(x1, x3, x4)
U54_gagga(x1, x2, x3, x4, x5, x6)  =  U54_gagga(x1, x3, x4, x6)
U55_gagga(x1, x2, x3, x4, x5, x6)  =  U55_gagga(x1, x2, x3, x4, x6)
appcF_in_ggga(x1, x2, x3, x4)  =  appcF_in_ggga(x1, x2, x3)
appcF_out_ggga(x1, x2, x3, x4)  =  appcF_out_ggga(x1, x2, x3, x4)
U53_ggga(x1, x2, x3, x4, x5, x6)  =  U53_ggga(x1, x2, x3, x4, x6)
qcD_out_gagga(x1, x2, x3, x4, x5)  =  qcD_out_gagga(x1, x2, x3, x4, x5)
U45_ga(x1, x2, x3)  =  U45_ga(x1, x3)
U46_ga(x1, x2, x3, x4)  =  U46_ga(x1, x3, x4)
U47_ga(x1, x2, x3)  =  U47_ga(x1, x3)
U41_ga(x1, x2, x3, x4, x5)  =  U41_ga(x1, x2, x3, x5)
QSC_IN_GA(x1, x2)  =  QSC_IN_GA(x1)
U18_GA(x1, x2, x3, x4, x5)  =  U18_GA(x1, x2, x3, x5)
LESSA_IN_GG(x1, x2)  =  LESSA_IN_GG(x1, x2)
U1_GG(x1, x2, x3)  =  U1_GG(x1, x2, x3)
U19_GA(x1, x2, x3, x4, x5)  =  U19_GA(x1, x2, x3, x5)
U20_GA(x1, x2, x3, x4, x5)  =  U20_GA(x1, x2, x3, x5)
PARTB_IN_GGAA(x1, x2, x3, x4)  =  PARTB_IN_GGAA(x1, x2)
U2_GGAA(x1, x2, x3, x4, x5, x6)  =  U2_GGAA(x1, x2, x3, x6)
U3_GGAA(x1, x2, x3, x4, x5, x6)  =  U3_GGAA(x1, x2, x3, x6)
U4_GGAA(x1, x2, x3, x4, x5, x6)  =  U4_GGAA(x1, x2, x3, x6)
U5_GGAA(x1, x2, x3, x4, x5, x6)  =  U5_GGAA(x1, x2, x3, x6)
U21_GA(x1, x2, x3, x4, x5)  =  U21_GA(x1, x2, x3, x5)
U22_GA(x1, x2, x3, x4, x5)  =  U22_GA(x1, x2, x3, x5)
U25_GA(x1, x2, x3, x4, x5)  =  U25_GA(x1, x2, x3, x5)
U26_GA(x1, x2, x3, x4, x5)  =  U26_GA(x1, x2, x3, x5)
U27_GA(x1, x2, x3, x4, x5)  =  U27_GA(x1, x2, x3, x5)
QSE_IN_GA(x1, x2)  =  QSE_IN_GA(x1)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x2, x4)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x2, x4)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x2, x4)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x4, x5)
U10_GA(x1, x2, x3, x4)  =  U10_GA(x1, x2, x4)
U11_GA(x1, x2, x3, x4, x5)  =  U11_GA(x1, x2, x4, x5)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x2, x4)
APPH_IN_GGGA(x1, x2, x3, x4)  =  APPH_IN_GGGA(x1, x2, x3)
U13_GGGA(x1, x2, x3, x4, x5, x6)  =  U13_GGGA(x1, x2, x3, x4, x6)
U28_GA(x1, x2, x3, x4, x5, x6)  =  U28_GA(x1, x2, x3, x5, x6)
U29_GA(x1, x2, x3, x4, x5)  =  U29_GA(x1, x2, x3, x5)
PD_IN_GAGGA(x1, x2, x3, x4, x5)  =  PD_IN_GAGGA(x1, x3, x4)
U15_GAGGA(x1, x2, x3, x4, x5, x6)  =  U15_GAGGA(x1, x3, x4, x6)
U16_GAGGA(x1, x2, x3, x4, x5, x6)  =  U16_GAGGA(x1, x3, x4, x6)
U17_GAGGA(x1, x2, x3, x4, x5, x6)  =  U17_GAGGA(x1, x3, x4, x6)
APPF_IN_GGGA(x1, x2, x3, x4)  =  APPF_IN_GGGA(x1, x2, x3)
U14_GGGA(x1, x2, x3, x4, x5, x6)  =  U14_GGGA(x1, x2, x3, x4, x6)
U30_GA(x1, x2, x3)  =  U30_GA(x1, x3)
U31_GA(x1, x2, x3, x4)  =  U31_GA(x1, x3, x4)
U32_GA(x1, x2, x3)  =  U32_GA(x1, x3)
U23_GA(x1, x2, x3, x4, x5, x6)  =  U23_GA(x1, x2, x3, x5, x6)
U24_GA(x1, x2, x3, x4, x5)  =  U24_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 39 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPF_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPF_IN_GGGA(X2, X3, X4, X5)

The TRS R consists of the following rules:

lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U34_gg(X1, X2, lesscA_in_gg(X1, X2))
U34_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U35_ggaa(X1, X2, X3, X4, X5, lesscA_in_gg(X1, X2))
U35_ggaa(X1, X2, X3, X4, X5, lesscA_out_gg(X1, X2)) → U36_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U37_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U37_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U36_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscE_in_ga([], []) → qscE_out_ga([], [])
qscE_in_ga(.(X1, X2), X3) → U48_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U48_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U49_ga(X1, X2, X3, X5, qscE_in_ga(X4, X6))
U49_ga(X1, X2, X3, X5, qscE_out_ga(X4, X6)) → U50_ga(X1, X2, X3, X6, qscE_in_ga(X5, X7))
U50_ga(X1, X2, X3, X6, qscE_out_ga(X5, X7)) → U51_ga(X1, X2, X3, appcH_in_ggga(X6, X1, X7, X3))
appcH_in_ggga([], X1, X2, .(X1, X2)) → appcH_out_ggga([], X1, X2, .(X1, X2))
appcH_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U52_ggga(X1, X2, X3, X4, X5, appcH_in_ggga(X2, X3, X4, X5))
U52_ggga(X1, X2, X3, X4, X5, appcH_out_ggga(X2, X3, X4, X5)) → appcH_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U51_ga(X1, X2, X3, appcH_out_ggga(X6, X1, X7, X3)) → qscE_out_ga(.(X1, X2), X3)
qscG_in_a([]) → qscG_out_a([])
qscC_in_ga([], []) → qscC_out_ga([], [])
qscC_in_ga(.(X1, .(X2, X3)), X4) → U38_ga(X1, X2, X3, X4, lesscA_in_gg(X1, X2))
U38_ga(X1, X2, X3, X4, lesscA_out_gg(X1, X2)) → U39_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U39_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U40_ga(X1, X2, X3, X4, X6, qscC_in_ga(.(X2, X5), X7))
qscC_in_ga(.(X1, .(X2, X3)), X4) → U42_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U42_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U43_ga(X1, X2, X3, X4, X6, qscE_in_ga(X5, X7))
U43_ga(X1, X2, X3, X4, X6, qscE_out_ga(X5, X7)) → U44_ga(X1, X2, X3, X4, qcD_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcD_in_gagga(X1, X2, X3, X4, X5) → U54_gagga(X1, X2, X3, X4, X5, qscE_in_ga(X1, X2))
U54_gagga(X1, X2, X3, X4, X5, qscE_out_ga(X1, X2)) → U55_gagga(X1, X2, X3, X4, X5, appcF_in_ggga(X3, X4, X2, X5))
appcF_in_ggga([], X1, X2, .(X1, X2)) → appcF_out_ggga([], X1, X2, .(X1, X2))
appcF_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U53_ggga(X1, X2, X3, X4, X5, appcF_in_ggga(X2, X3, X4, X5))
U53_ggga(X1, X2, X3, X4, X5, appcF_out_ggga(X2, X3, X4, X5)) → appcF_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U55_gagga(X1, X2, X3, X4, X5, appcF_out_ggga(X3, X4, X2, X5)) → qcD_out_gagga(X1, X2, X3, X4, X5)
U44_ga(X1, X2, X3, X4, qcD_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscC_out_ga(.(X1, .(X2, X3)), X4)
qscC_in_ga(.(X1, []), X2) → U45_ga(X1, X2, qscG_in_a(X3))
U45_ga(X1, X2, qscG_out_a(X3)) → U46_ga(X1, X2, X3, qscG_in_a(X4))
U46_ga(X1, X2, X3, qscG_out_a(X4)) → U47_ga(X1, X2, appcF_in_ggga(X3, X1, X4, X2))
U47_ga(X1, X2, appcF_out_ggga(X3, X1, X4, X2)) → qscC_out_ga(.(X1, []), X2)
U40_ga(X1, X2, X3, X4, X6, qscC_out_ga(.(X2, X5), X7)) → U41_ga(X1, X2, X3, X4, qcD_in_gagga(X6, X8, X7, X1, X4))
U41_ga(X1, X2, X3, X4, qcD_out_gagga(X6, X8, X7, X1, X4)) → qscC_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
0  =  0
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U34_gg(x1, x2, x3)  =  U34_gg(x1, x2, x3)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U35_ggaa(x1, x2, x3, x4, x5, x6)  =  U35_ggaa(x1, x2, x3, x6)
U36_ggaa(x1, x2, x3, x4, x5, x6)  =  U36_ggaa(x1, x2, x3, x6)
U37_ggaa(x1, x2, x3, x4, x5, x6)  =  U37_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qscE_in_ga(x1, x2)  =  qscE_in_ga(x1)
qscE_out_ga(x1, x2)  =  qscE_out_ga(x1, x2)
U48_ga(x1, x2, x3, x4)  =  U48_ga(x1, x2, x4)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x4, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x4, x5)
U51_ga(x1, x2, x3, x4)  =  U51_ga(x1, x2, x4)
appcH_in_ggga(x1, x2, x3, x4)  =  appcH_in_ggga(x1, x2, x3)
appcH_out_ggga(x1, x2, x3, x4)  =  appcH_out_ggga(x1, x2, x3, x4)
U52_ggga(x1, x2, x3, x4, x5, x6)  =  U52_ggga(x1, x2, x3, x4, x6)
qscG_in_a(x1)  =  qscG_in_a
qscG_out_a(x1)  =  qscG_out_a(x1)
qscC_in_ga(x1, x2)  =  qscC_in_ga(x1)
qscC_out_ga(x1, x2)  =  qscC_out_ga(x1, x2)
U38_ga(x1, x2, x3, x4, x5)  =  U38_ga(x1, x2, x3, x5)
U39_ga(x1, x2, x3, x4, x5)  =  U39_ga(x1, x2, x3, x5)
U40_ga(x1, x2, x3, x4, x5, x6)  =  U40_ga(x1, x2, x3, x5, x6)
U42_ga(x1, x2, x3, x4, x5)  =  U42_ga(x1, x2, x3, x5)
U43_ga(x1, x2, x3, x4, x5, x6)  =  U43_ga(x1, x2, x3, x5, x6)
U44_ga(x1, x2, x3, x4, x5)  =  U44_ga(x1, x2, x3, x5)
qcD_in_gagga(x1, x2, x3, x4, x5)  =  qcD_in_gagga(x1, x3, x4)
U54_gagga(x1, x2, x3, x4, x5, x6)  =  U54_gagga(x1, x3, x4, x6)
U55_gagga(x1, x2, x3, x4, x5, x6)  =  U55_gagga(x1, x2, x3, x4, x6)
appcF_in_ggga(x1, x2, x3, x4)  =  appcF_in_ggga(x1, x2, x3)
appcF_out_ggga(x1, x2, x3, x4)  =  appcF_out_ggga(x1, x2, x3, x4)
U53_ggga(x1, x2, x3, x4, x5, x6)  =  U53_ggga(x1, x2, x3, x4, x6)
qcD_out_gagga(x1, x2, x3, x4, x5)  =  qcD_out_gagga(x1, x2, x3, x4, x5)
U45_ga(x1, x2, x3)  =  U45_ga(x1, x3)
U46_ga(x1, x2, x3, x4)  =  U46_ga(x1, x3, x4)
U47_ga(x1, x2, x3)  =  U47_ga(x1, x3)
U41_ga(x1, x2, x3, x4, x5)  =  U41_ga(x1, x2, x3, x5)
APPF_IN_GGGA(x1, x2, x3, x4)  =  APPF_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPF_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPF_IN_GGGA(X2, X3, X4, X5)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APPF_IN_GGGA(x1, x2, x3, x4)  =  APPF_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPF_IN_GGGA(.(X1, X2), X3, X4) → APPF_IN_GGGA(X2, X3, X4)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPF_IN_GGGA(.(X1, X2), X3, X4) → APPF_IN_GGGA(X2, X3, X4)
    The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPH_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPH_IN_GGGA(X2, X3, X4, X5)

The TRS R consists of the following rules:

lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U34_gg(X1, X2, lesscA_in_gg(X1, X2))
U34_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U35_ggaa(X1, X2, X3, X4, X5, lesscA_in_gg(X1, X2))
U35_ggaa(X1, X2, X3, X4, X5, lesscA_out_gg(X1, X2)) → U36_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U37_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U37_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U36_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscE_in_ga([], []) → qscE_out_ga([], [])
qscE_in_ga(.(X1, X2), X3) → U48_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U48_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U49_ga(X1, X2, X3, X5, qscE_in_ga(X4, X6))
U49_ga(X1, X2, X3, X5, qscE_out_ga(X4, X6)) → U50_ga(X1, X2, X3, X6, qscE_in_ga(X5, X7))
U50_ga(X1, X2, X3, X6, qscE_out_ga(X5, X7)) → U51_ga(X1, X2, X3, appcH_in_ggga(X6, X1, X7, X3))
appcH_in_ggga([], X1, X2, .(X1, X2)) → appcH_out_ggga([], X1, X2, .(X1, X2))
appcH_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U52_ggga(X1, X2, X3, X4, X5, appcH_in_ggga(X2, X3, X4, X5))
U52_ggga(X1, X2, X3, X4, X5, appcH_out_ggga(X2, X3, X4, X5)) → appcH_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U51_ga(X1, X2, X3, appcH_out_ggga(X6, X1, X7, X3)) → qscE_out_ga(.(X1, X2), X3)
qscG_in_a([]) → qscG_out_a([])
qscC_in_ga([], []) → qscC_out_ga([], [])
qscC_in_ga(.(X1, .(X2, X3)), X4) → U38_ga(X1, X2, X3, X4, lesscA_in_gg(X1, X2))
U38_ga(X1, X2, X3, X4, lesscA_out_gg(X1, X2)) → U39_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U39_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U40_ga(X1, X2, X3, X4, X6, qscC_in_ga(.(X2, X5), X7))
qscC_in_ga(.(X1, .(X2, X3)), X4) → U42_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U42_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U43_ga(X1, X2, X3, X4, X6, qscE_in_ga(X5, X7))
U43_ga(X1, X2, X3, X4, X6, qscE_out_ga(X5, X7)) → U44_ga(X1, X2, X3, X4, qcD_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcD_in_gagga(X1, X2, X3, X4, X5) → U54_gagga(X1, X2, X3, X4, X5, qscE_in_ga(X1, X2))
U54_gagga(X1, X2, X3, X4, X5, qscE_out_ga(X1, X2)) → U55_gagga(X1, X2, X3, X4, X5, appcF_in_ggga(X3, X4, X2, X5))
appcF_in_ggga([], X1, X2, .(X1, X2)) → appcF_out_ggga([], X1, X2, .(X1, X2))
appcF_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U53_ggga(X1, X2, X3, X4, X5, appcF_in_ggga(X2, X3, X4, X5))
U53_ggga(X1, X2, X3, X4, X5, appcF_out_ggga(X2, X3, X4, X5)) → appcF_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U55_gagga(X1, X2, X3, X4, X5, appcF_out_ggga(X3, X4, X2, X5)) → qcD_out_gagga(X1, X2, X3, X4, X5)
U44_ga(X1, X2, X3, X4, qcD_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscC_out_ga(.(X1, .(X2, X3)), X4)
qscC_in_ga(.(X1, []), X2) → U45_ga(X1, X2, qscG_in_a(X3))
U45_ga(X1, X2, qscG_out_a(X3)) → U46_ga(X1, X2, X3, qscG_in_a(X4))
U46_ga(X1, X2, X3, qscG_out_a(X4)) → U47_ga(X1, X2, appcF_in_ggga(X3, X1, X4, X2))
U47_ga(X1, X2, appcF_out_ggga(X3, X1, X4, X2)) → qscC_out_ga(.(X1, []), X2)
U40_ga(X1, X2, X3, X4, X6, qscC_out_ga(.(X2, X5), X7)) → U41_ga(X1, X2, X3, X4, qcD_in_gagga(X6, X8, X7, X1, X4))
U41_ga(X1, X2, X3, X4, qcD_out_gagga(X6, X8, X7, X1, X4)) → qscC_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
0  =  0
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U34_gg(x1, x2, x3)  =  U34_gg(x1, x2, x3)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U35_ggaa(x1, x2, x3, x4, x5, x6)  =  U35_ggaa(x1, x2, x3, x6)
U36_ggaa(x1, x2, x3, x4, x5, x6)  =  U36_ggaa(x1, x2, x3, x6)
U37_ggaa(x1, x2, x3, x4, x5, x6)  =  U37_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qscE_in_ga(x1, x2)  =  qscE_in_ga(x1)
qscE_out_ga(x1, x2)  =  qscE_out_ga(x1, x2)
U48_ga(x1, x2, x3, x4)  =  U48_ga(x1, x2, x4)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x4, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x4, x5)
U51_ga(x1, x2, x3, x4)  =  U51_ga(x1, x2, x4)
appcH_in_ggga(x1, x2, x3, x4)  =  appcH_in_ggga(x1, x2, x3)
appcH_out_ggga(x1, x2, x3, x4)  =  appcH_out_ggga(x1, x2, x3, x4)
U52_ggga(x1, x2, x3, x4, x5, x6)  =  U52_ggga(x1, x2, x3, x4, x6)
qscG_in_a(x1)  =  qscG_in_a
qscG_out_a(x1)  =  qscG_out_a(x1)
qscC_in_ga(x1, x2)  =  qscC_in_ga(x1)
qscC_out_ga(x1, x2)  =  qscC_out_ga(x1, x2)
U38_ga(x1, x2, x3, x4, x5)  =  U38_ga(x1, x2, x3, x5)
U39_ga(x1, x2, x3, x4, x5)  =  U39_ga(x1, x2, x3, x5)
U40_ga(x1, x2, x3, x4, x5, x6)  =  U40_ga(x1, x2, x3, x5, x6)
U42_ga(x1, x2, x3, x4, x5)  =  U42_ga(x1, x2, x3, x5)
U43_ga(x1, x2, x3, x4, x5, x6)  =  U43_ga(x1, x2, x3, x5, x6)
U44_ga(x1, x2, x3, x4, x5)  =  U44_ga(x1, x2, x3, x5)
qcD_in_gagga(x1, x2, x3, x4, x5)  =  qcD_in_gagga(x1, x3, x4)
U54_gagga(x1, x2, x3, x4, x5, x6)  =  U54_gagga(x1, x3, x4, x6)
U55_gagga(x1, x2, x3, x4, x5, x6)  =  U55_gagga(x1, x2, x3, x4, x6)
appcF_in_ggga(x1, x2, x3, x4)  =  appcF_in_ggga(x1, x2, x3)
appcF_out_ggga(x1, x2, x3, x4)  =  appcF_out_ggga(x1, x2, x3, x4)
U53_ggga(x1, x2, x3, x4, x5, x6)  =  U53_ggga(x1, x2, x3, x4, x6)
qcD_out_gagga(x1, x2, x3, x4, x5)  =  qcD_out_gagga(x1, x2, x3, x4, x5)
U45_ga(x1, x2, x3)  =  U45_ga(x1, x3)
U46_ga(x1, x2, x3, x4)  =  U46_ga(x1, x3, x4)
U47_ga(x1, x2, x3)  =  U47_ga(x1, x3)
U41_ga(x1, x2, x3, x4, x5)  =  U41_ga(x1, x2, x3, x5)
APPH_IN_GGGA(x1, x2, x3, x4)  =  APPH_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPH_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPH_IN_GGGA(X2, X3, X4, X5)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APPH_IN_GGGA(x1, x2, x3, x4)  =  APPH_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPH_IN_GGGA(.(X1, X2), X3, X4) → APPH_IN_GGGA(X2, X3, X4)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPH_IN_GGGA(.(X1, X2), X3, X4) → APPH_IN_GGGA(X2, X3, X4)
    The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3

(22) YES

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSA_IN_GG(s(X1), s(X2)) → LESSA_IN_GG(X1, X2)

The TRS R consists of the following rules:

lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U34_gg(X1, X2, lesscA_in_gg(X1, X2))
U34_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U35_ggaa(X1, X2, X3, X4, X5, lesscA_in_gg(X1, X2))
U35_ggaa(X1, X2, X3, X4, X5, lesscA_out_gg(X1, X2)) → U36_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U37_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U37_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U36_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscE_in_ga([], []) → qscE_out_ga([], [])
qscE_in_ga(.(X1, X2), X3) → U48_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U48_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U49_ga(X1, X2, X3, X5, qscE_in_ga(X4, X6))
U49_ga(X1, X2, X3, X5, qscE_out_ga(X4, X6)) → U50_ga(X1, X2, X3, X6, qscE_in_ga(X5, X7))
U50_ga(X1, X2, X3, X6, qscE_out_ga(X5, X7)) → U51_ga(X1, X2, X3, appcH_in_ggga(X6, X1, X7, X3))
appcH_in_ggga([], X1, X2, .(X1, X2)) → appcH_out_ggga([], X1, X2, .(X1, X2))
appcH_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U52_ggga(X1, X2, X3, X4, X5, appcH_in_ggga(X2, X3, X4, X5))
U52_ggga(X1, X2, X3, X4, X5, appcH_out_ggga(X2, X3, X4, X5)) → appcH_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U51_ga(X1, X2, X3, appcH_out_ggga(X6, X1, X7, X3)) → qscE_out_ga(.(X1, X2), X3)
qscG_in_a([]) → qscG_out_a([])
qscC_in_ga([], []) → qscC_out_ga([], [])
qscC_in_ga(.(X1, .(X2, X3)), X4) → U38_ga(X1, X2, X3, X4, lesscA_in_gg(X1, X2))
U38_ga(X1, X2, X3, X4, lesscA_out_gg(X1, X2)) → U39_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U39_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U40_ga(X1, X2, X3, X4, X6, qscC_in_ga(.(X2, X5), X7))
qscC_in_ga(.(X1, .(X2, X3)), X4) → U42_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U42_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U43_ga(X1, X2, X3, X4, X6, qscE_in_ga(X5, X7))
U43_ga(X1, X2, X3, X4, X6, qscE_out_ga(X5, X7)) → U44_ga(X1, X2, X3, X4, qcD_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcD_in_gagga(X1, X2, X3, X4, X5) → U54_gagga(X1, X2, X3, X4, X5, qscE_in_ga(X1, X2))
U54_gagga(X1, X2, X3, X4, X5, qscE_out_ga(X1, X2)) → U55_gagga(X1, X2, X3, X4, X5, appcF_in_ggga(X3, X4, X2, X5))
appcF_in_ggga([], X1, X2, .(X1, X2)) → appcF_out_ggga([], X1, X2, .(X1, X2))
appcF_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U53_ggga(X1, X2, X3, X4, X5, appcF_in_ggga(X2, X3, X4, X5))
U53_ggga(X1, X2, X3, X4, X5, appcF_out_ggga(X2, X3, X4, X5)) → appcF_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U55_gagga(X1, X2, X3, X4, X5, appcF_out_ggga(X3, X4, X2, X5)) → qcD_out_gagga(X1, X2, X3, X4, X5)
U44_ga(X1, X2, X3, X4, qcD_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscC_out_ga(.(X1, .(X2, X3)), X4)
qscC_in_ga(.(X1, []), X2) → U45_ga(X1, X2, qscG_in_a(X3))
U45_ga(X1, X2, qscG_out_a(X3)) → U46_ga(X1, X2, X3, qscG_in_a(X4))
U46_ga(X1, X2, X3, qscG_out_a(X4)) → U47_ga(X1, X2, appcF_in_ggga(X3, X1, X4, X2))
U47_ga(X1, X2, appcF_out_ggga(X3, X1, X4, X2)) → qscC_out_ga(.(X1, []), X2)
U40_ga(X1, X2, X3, X4, X6, qscC_out_ga(.(X2, X5), X7)) → U41_ga(X1, X2, X3, X4, qcD_in_gagga(X6, X8, X7, X1, X4))
U41_ga(X1, X2, X3, X4, qcD_out_gagga(X6, X8, X7, X1, X4)) → qscC_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
0  =  0
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U34_gg(x1, x2, x3)  =  U34_gg(x1, x2, x3)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U35_ggaa(x1, x2, x3, x4, x5, x6)  =  U35_ggaa(x1, x2, x3, x6)
U36_ggaa(x1, x2, x3, x4, x5, x6)  =  U36_ggaa(x1, x2, x3, x6)
U37_ggaa(x1, x2, x3, x4, x5, x6)  =  U37_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qscE_in_ga(x1, x2)  =  qscE_in_ga(x1)
qscE_out_ga(x1, x2)  =  qscE_out_ga(x1, x2)
U48_ga(x1, x2, x3, x4)  =  U48_ga(x1, x2, x4)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x4, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x4, x5)
U51_ga(x1, x2, x3, x4)  =  U51_ga(x1, x2, x4)
appcH_in_ggga(x1, x2, x3, x4)  =  appcH_in_ggga(x1, x2, x3)
appcH_out_ggga(x1, x2, x3, x4)  =  appcH_out_ggga(x1, x2, x3, x4)
U52_ggga(x1, x2, x3, x4, x5, x6)  =  U52_ggga(x1, x2, x3, x4, x6)
qscG_in_a(x1)  =  qscG_in_a
qscG_out_a(x1)  =  qscG_out_a(x1)
qscC_in_ga(x1, x2)  =  qscC_in_ga(x1)
qscC_out_ga(x1, x2)  =  qscC_out_ga(x1, x2)
U38_ga(x1, x2, x3, x4, x5)  =  U38_ga(x1, x2, x3, x5)
U39_ga(x1, x2, x3, x4, x5)  =  U39_ga(x1, x2, x3, x5)
U40_ga(x1, x2, x3, x4, x5, x6)  =  U40_ga(x1, x2, x3, x5, x6)
U42_ga(x1, x2, x3, x4, x5)  =  U42_ga(x1, x2, x3, x5)
U43_ga(x1, x2, x3, x4, x5, x6)  =  U43_ga(x1, x2, x3, x5, x6)
U44_ga(x1, x2, x3, x4, x5)  =  U44_ga(x1, x2, x3, x5)
qcD_in_gagga(x1, x2, x3, x4, x5)  =  qcD_in_gagga(x1, x3, x4)
U54_gagga(x1, x2, x3, x4, x5, x6)  =  U54_gagga(x1, x3, x4, x6)
U55_gagga(x1, x2, x3, x4, x5, x6)  =  U55_gagga(x1, x2, x3, x4, x6)
appcF_in_ggga(x1, x2, x3, x4)  =  appcF_in_ggga(x1, x2, x3)
appcF_out_ggga(x1, x2, x3, x4)  =  appcF_out_ggga(x1, x2, x3, x4)
U53_ggga(x1, x2, x3, x4, x5, x6)  =  U53_ggga(x1, x2, x3, x4, x6)
qcD_out_gagga(x1, x2, x3, x4, x5)  =  qcD_out_gagga(x1, x2, x3, x4, x5)
U45_ga(x1, x2, x3)  =  U45_ga(x1, x3)
U46_ga(x1, x2, x3, x4)  =  U46_ga(x1, x3, x4)
U47_ga(x1, x2, x3)  =  U47_ga(x1, x3)
U41_ga(x1, x2, x3, x4, x5)  =  U41_ga(x1, x2, x3, x5)
LESSA_IN_GG(x1, x2)  =  LESSA_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSA_IN_GG(s(X1), s(X2)) → LESSA_IN_GG(X1, X2)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(26) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSA_IN_GG(s(X1), s(X2)) → LESSA_IN_GG(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(28) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LESSA_IN_GG(s(X1), s(X2)) → LESSA_IN_GG(X1, X2)
    The graph contains the following edges 1 > 1, 2 > 2

(29) YES

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → U3_GGAA(X1, X2, X3, X4, X5, lesscA_in_gg(X1, X2))
U3_GGAA(X1, X2, X3, X4, X5, lesscA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → PARTB_IN_GGAA(X1, X3, X4, X5)

The TRS R consists of the following rules:

lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U34_gg(X1, X2, lesscA_in_gg(X1, X2))
U34_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U35_ggaa(X1, X2, X3, X4, X5, lesscA_in_gg(X1, X2))
U35_ggaa(X1, X2, X3, X4, X5, lesscA_out_gg(X1, X2)) → U36_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U37_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U37_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U36_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscE_in_ga([], []) → qscE_out_ga([], [])
qscE_in_ga(.(X1, X2), X3) → U48_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U48_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U49_ga(X1, X2, X3, X5, qscE_in_ga(X4, X6))
U49_ga(X1, X2, X3, X5, qscE_out_ga(X4, X6)) → U50_ga(X1, X2, X3, X6, qscE_in_ga(X5, X7))
U50_ga(X1, X2, X3, X6, qscE_out_ga(X5, X7)) → U51_ga(X1, X2, X3, appcH_in_ggga(X6, X1, X7, X3))
appcH_in_ggga([], X1, X2, .(X1, X2)) → appcH_out_ggga([], X1, X2, .(X1, X2))
appcH_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U52_ggga(X1, X2, X3, X4, X5, appcH_in_ggga(X2, X3, X4, X5))
U52_ggga(X1, X2, X3, X4, X5, appcH_out_ggga(X2, X3, X4, X5)) → appcH_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U51_ga(X1, X2, X3, appcH_out_ggga(X6, X1, X7, X3)) → qscE_out_ga(.(X1, X2), X3)
qscG_in_a([]) → qscG_out_a([])
qscC_in_ga([], []) → qscC_out_ga([], [])
qscC_in_ga(.(X1, .(X2, X3)), X4) → U38_ga(X1, X2, X3, X4, lesscA_in_gg(X1, X2))
U38_ga(X1, X2, X3, X4, lesscA_out_gg(X1, X2)) → U39_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U39_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U40_ga(X1, X2, X3, X4, X6, qscC_in_ga(.(X2, X5), X7))
qscC_in_ga(.(X1, .(X2, X3)), X4) → U42_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U42_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U43_ga(X1, X2, X3, X4, X6, qscE_in_ga(X5, X7))
U43_ga(X1, X2, X3, X4, X6, qscE_out_ga(X5, X7)) → U44_ga(X1, X2, X3, X4, qcD_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcD_in_gagga(X1, X2, X3, X4, X5) → U54_gagga(X1, X2, X3, X4, X5, qscE_in_ga(X1, X2))
U54_gagga(X1, X2, X3, X4, X5, qscE_out_ga(X1, X2)) → U55_gagga(X1, X2, X3, X4, X5, appcF_in_ggga(X3, X4, X2, X5))
appcF_in_ggga([], X1, X2, .(X1, X2)) → appcF_out_ggga([], X1, X2, .(X1, X2))
appcF_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U53_ggga(X1, X2, X3, X4, X5, appcF_in_ggga(X2, X3, X4, X5))
U53_ggga(X1, X2, X3, X4, X5, appcF_out_ggga(X2, X3, X4, X5)) → appcF_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U55_gagga(X1, X2, X3, X4, X5, appcF_out_ggga(X3, X4, X2, X5)) → qcD_out_gagga(X1, X2, X3, X4, X5)
U44_ga(X1, X2, X3, X4, qcD_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscC_out_ga(.(X1, .(X2, X3)), X4)
qscC_in_ga(.(X1, []), X2) → U45_ga(X1, X2, qscG_in_a(X3))
U45_ga(X1, X2, qscG_out_a(X3)) → U46_ga(X1, X2, X3, qscG_in_a(X4))
U46_ga(X1, X2, X3, qscG_out_a(X4)) → U47_ga(X1, X2, appcF_in_ggga(X3, X1, X4, X2))
U47_ga(X1, X2, appcF_out_ggga(X3, X1, X4, X2)) → qscC_out_ga(.(X1, []), X2)
U40_ga(X1, X2, X3, X4, X6, qscC_out_ga(.(X2, X5), X7)) → U41_ga(X1, X2, X3, X4, qcD_in_gagga(X6, X8, X7, X1, X4))
U41_ga(X1, X2, X3, X4, qcD_out_gagga(X6, X8, X7, X1, X4)) → qscC_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
0  =  0
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U34_gg(x1, x2, x3)  =  U34_gg(x1, x2, x3)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U35_ggaa(x1, x2, x3, x4, x5, x6)  =  U35_ggaa(x1, x2, x3, x6)
U36_ggaa(x1, x2, x3, x4, x5, x6)  =  U36_ggaa(x1, x2, x3, x6)
U37_ggaa(x1, x2, x3, x4, x5, x6)  =  U37_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qscE_in_ga(x1, x2)  =  qscE_in_ga(x1)
qscE_out_ga(x1, x2)  =  qscE_out_ga(x1, x2)
U48_ga(x1, x2, x3, x4)  =  U48_ga(x1, x2, x4)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x4, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x4, x5)
U51_ga(x1, x2, x3, x4)  =  U51_ga(x1, x2, x4)
appcH_in_ggga(x1, x2, x3, x4)  =  appcH_in_ggga(x1, x2, x3)
appcH_out_ggga(x1, x2, x3, x4)  =  appcH_out_ggga(x1, x2, x3, x4)
U52_ggga(x1, x2, x3, x4, x5, x6)  =  U52_ggga(x1, x2, x3, x4, x6)
qscG_in_a(x1)  =  qscG_in_a
qscG_out_a(x1)  =  qscG_out_a(x1)
qscC_in_ga(x1, x2)  =  qscC_in_ga(x1)
qscC_out_ga(x1, x2)  =  qscC_out_ga(x1, x2)
U38_ga(x1, x2, x3, x4, x5)  =  U38_ga(x1, x2, x3, x5)
U39_ga(x1, x2, x3, x4, x5)  =  U39_ga(x1, x2, x3, x5)
U40_ga(x1, x2, x3, x4, x5, x6)  =  U40_ga(x1, x2, x3, x5, x6)
U42_ga(x1, x2, x3, x4, x5)  =  U42_ga(x1, x2, x3, x5)
U43_ga(x1, x2, x3, x4, x5, x6)  =  U43_ga(x1, x2, x3, x5, x6)
U44_ga(x1, x2, x3, x4, x5)  =  U44_ga(x1, x2, x3, x5)
qcD_in_gagga(x1, x2, x3, x4, x5)  =  qcD_in_gagga(x1, x3, x4)
U54_gagga(x1, x2, x3, x4, x5, x6)  =  U54_gagga(x1, x3, x4, x6)
U55_gagga(x1, x2, x3, x4, x5, x6)  =  U55_gagga(x1, x2, x3, x4, x6)
appcF_in_ggga(x1, x2, x3, x4)  =  appcF_in_ggga(x1, x2, x3)
appcF_out_ggga(x1, x2, x3, x4)  =  appcF_out_ggga(x1, x2, x3, x4)
U53_ggga(x1, x2, x3, x4, x5, x6)  =  U53_ggga(x1, x2, x3, x4, x6)
qcD_out_gagga(x1, x2, x3, x4, x5)  =  qcD_out_gagga(x1, x2, x3, x4, x5)
U45_ga(x1, x2, x3)  =  U45_ga(x1, x3)
U46_ga(x1, x2, x3, x4)  =  U46_ga(x1, x3, x4)
U47_ga(x1, x2, x3)  =  U47_ga(x1, x3)
U41_ga(x1, x2, x3, x4, x5)  =  U41_ga(x1, x2, x3, x5)
PARTB_IN_GGAA(x1, x2, x3, x4)  =  PARTB_IN_GGAA(x1, x2)
U3_GGAA(x1, x2, x3, x4, x5, x6)  =  U3_GGAA(x1, x2, x3, x6)

We have to consider all (P,R,Pi)-chains

(31) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(32) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → U3_GGAA(X1, X2, X3, X4, X5, lesscA_in_gg(X1, X2))
U3_GGAA(X1, X2, X3, X4, X5, lesscA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → PARTB_IN_GGAA(X1, X3, X4, X5)

The TRS R consists of the following rules:

lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U34_gg(X1, X2, lesscA_in_gg(X1, X2))
U34_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
0  =  0
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U34_gg(x1, x2, x3)  =  U34_gg(x1, x2, x3)
PARTB_IN_GGAA(x1, x2, x3, x4)  =  PARTB_IN_GGAA(x1, x2)
U3_GGAA(x1, x2, x3, x4, x5, x6)  =  U3_GGAA(x1, x2, x3, x6)

We have to consider all (P,R,Pi)-chains

(33) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PARTB_IN_GGAA(X1, .(X2, X3)) → U3_GGAA(X1, X2, X3, lesscA_in_gg(X1, X2))
U3_GGAA(X1, X2, X3, lesscA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3)
PARTB_IN_GGAA(X1, .(X2, X3)) → PARTB_IN_GGAA(X1, X3)

The TRS R consists of the following rules:

lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U34_gg(X1, X2, lesscA_in_gg(X1, X2))
U34_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

lesscA_in_gg(x0, x1)
U34_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(35) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • U3_GGAA(X1, X2, X3, lesscA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3)
    The graph contains the following edges 1 >= 1, 4 > 1, 3 >= 2

  • PARTB_IN_GGAA(X1, .(X2, X3)) → PARTB_IN_GGAA(X1, X3)
    The graph contains the following edges 1 >= 1, 2 > 2

  • PARTB_IN_GGAA(X1, .(X2, X3)) → U3_GGAA(X1, X2, X3, lesscA_in_gg(X1, X2))
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

(36) YES

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QSE_IN_GA(.(X1, X2), X3) → U7_GA(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U7_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → QSE_IN_GA(X4, X6)
U7_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U9_GA(X1, X2, X3, X5, qscE_in_ga(X4, X6))
U9_GA(X1, X2, X3, X5, qscE_out_ga(X4, X6)) → QSE_IN_GA(X5, X7)

The TRS R consists of the following rules:

lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U34_gg(X1, X2, lesscA_in_gg(X1, X2))
U34_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U35_ggaa(X1, X2, X3, X4, X5, lesscA_in_gg(X1, X2))
U35_ggaa(X1, X2, X3, X4, X5, lesscA_out_gg(X1, X2)) → U36_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U37_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U37_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U36_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscE_in_ga([], []) → qscE_out_ga([], [])
qscE_in_ga(.(X1, X2), X3) → U48_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U48_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U49_ga(X1, X2, X3, X5, qscE_in_ga(X4, X6))
U49_ga(X1, X2, X3, X5, qscE_out_ga(X4, X6)) → U50_ga(X1, X2, X3, X6, qscE_in_ga(X5, X7))
U50_ga(X1, X2, X3, X6, qscE_out_ga(X5, X7)) → U51_ga(X1, X2, X3, appcH_in_ggga(X6, X1, X7, X3))
appcH_in_ggga([], X1, X2, .(X1, X2)) → appcH_out_ggga([], X1, X2, .(X1, X2))
appcH_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U52_ggga(X1, X2, X3, X4, X5, appcH_in_ggga(X2, X3, X4, X5))
U52_ggga(X1, X2, X3, X4, X5, appcH_out_ggga(X2, X3, X4, X5)) → appcH_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U51_ga(X1, X2, X3, appcH_out_ggga(X6, X1, X7, X3)) → qscE_out_ga(.(X1, X2), X3)
qscG_in_a([]) → qscG_out_a([])
qscC_in_ga([], []) → qscC_out_ga([], [])
qscC_in_ga(.(X1, .(X2, X3)), X4) → U38_ga(X1, X2, X3, X4, lesscA_in_gg(X1, X2))
U38_ga(X1, X2, X3, X4, lesscA_out_gg(X1, X2)) → U39_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U39_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U40_ga(X1, X2, X3, X4, X6, qscC_in_ga(.(X2, X5), X7))
qscC_in_ga(.(X1, .(X2, X3)), X4) → U42_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U42_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U43_ga(X1, X2, X3, X4, X6, qscE_in_ga(X5, X7))
U43_ga(X1, X2, X3, X4, X6, qscE_out_ga(X5, X7)) → U44_ga(X1, X2, X3, X4, qcD_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcD_in_gagga(X1, X2, X3, X4, X5) → U54_gagga(X1, X2, X3, X4, X5, qscE_in_ga(X1, X2))
U54_gagga(X1, X2, X3, X4, X5, qscE_out_ga(X1, X2)) → U55_gagga(X1, X2, X3, X4, X5, appcF_in_ggga(X3, X4, X2, X5))
appcF_in_ggga([], X1, X2, .(X1, X2)) → appcF_out_ggga([], X1, X2, .(X1, X2))
appcF_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U53_ggga(X1, X2, X3, X4, X5, appcF_in_ggga(X2, X3, X4, X5))
U53_ggga(X1, X2, X3, X4, X5, appcF_out_ggga(X2, X3, X4, X5)) → appcF_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U55_gagga(X1, X2, X3, X4, X5, appcF_out_ggga(X3, X4, X2, X5)) → qcD_out_gagga(X1, X2, X3, X4, X5)
U44_ga(X1, X2, X3, X4, qcD_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscC_out_ga(.(X1, .(X2, X3)), X4)
qscC_in_ga(.(X1, []), X2) → U45_ga(X1, X2, qscG_in_a(X3))
U45_ga(X1, X2, qscG_out_a(X3)) → U46_ga(X1, X2, X3, qscG_in_a(X4))
U46_ga(X1, X2, X3, qscG_out_a(X4)) → U47_ga(X1, X2, appcF_in_ggga(X3, X1, X4, X2))
U47_ga(X1, X2, appcF_out_ggga(X3, X1, X4, X2)) → qscC_out_ga(.(X1, []), X2)
U40_ga(X1, X2, X3, X4, X6, qscC_out_ga(.(X2, X5), X7)) → U41_ga(X1, X2, X3, X4, qcD_in_gagga(X6, X8, X7, X1, X4))
U41_ga(X1, X2, X3, X4, qcD_out_gagga(X6, X8, X7, X1, X4)) → qscC_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
0  =  0
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U34_gg(x1, x2, x3)  =  U34_gg(x1, x2, x3)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U35_ggaa(x1, x2, x3, x4, x5, x6)  =  U35_ggaa(x1, x2, x3, x6)
U36_ggaa(x1, x2, x3, x4, x5, x6)  =  U36_ggaa(x1, x2, x3, x6)
U37_ggaa(x1, x2, x3, x4, x5, x6)  =  U37_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qscE_in_ga(x1, x2)  =  qscE_in_ga(x1)
qscE_out_ga(x1, x2)  =  qscE_out_ga(x1, x2)
U48_ga(x1, x2, x3, x4)  =  U48_ga(x1, x2, x4)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x4, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x4, x5)
U51_ga(x1, x2, x3, x4)  =  U51_ga(x1, x2, x4)
appcH_in_ggga(x1, x2, x3, x4)  =  appcH_in_ggga(x1, x2, x3)
appcH_out_ggga(x1, x2, x3, x4)  =  appcH_out_ggga(x1, x2, x3, x4)
U52_ggga(x1, x2, x3, x4, x5, x6)  =  U52_ggga(x1, x2, x3, x4, x6)
qscG_in_a(x1)  =  qscG_in_a
qscG_out_a(x1)  =  qscG_out_a(x1)
qscC_in_ga(x1, x2)  =  qscC_in_ga(x1)
qscC_out_ga(x1, x2)  =  qscC_out_ga(x1, x2)
U38_ga(x1, x2, x3, x4, x5)  =  U38_ga(x1, x2, x3, x5)
U39_ga(x1, x2, x3, x4, x5)  =  U39_ga(x1, x2, x3, x5)
U40_ga(x1, x2, x3, x4, x5, x6)  =  U40_ga(x1, x2, x3, x5, x6)
U42_ga(x1, x2, x3, x4, x5)  =  U42_ga(x1, x2, x3, x5)
U43_ga(x1, x2, x3, x4, x5, x6)  =  U43_ga(x1, x2, x3, x5, x6)
U44_ga(x1, x2, x3, x4, x5)  =  U44_ga(x1, x2, x3, x5)
qcD_in_gagga(x1, x2, x3, x4, x5)  =  qcD_in_gagga(x1, x3, x4)
U54_gagga(x1, x2, x3, x4, x5, x6)  =  U54_gagga(x1, x3, x4, x6)
U55_gagga(x1, x2, x3, x4, x5, x6)  =  U55_gagga(x1, x2, x3, x4, x6)
appcF_in_ggga(x1, x2, x3, x4)  =  appcF_in_ggga(x1, x2, x3)
appcF_out_ggga(x1, x2, x3, x4)  =  appcF_out_ggga(x1, x2, x3, x4)
U53_ggga(x1, x2, x3, x4, x5, x6)  =  U53_ggga(x1, x2, x3, x4, x6)
qcD_out_gagga(x1, x2, x3, x4, x5)  =  qcD_out_gagga(x1, x2, x3, x4, x5)
U45_ga(x1, x2, x3)  =  U45_ga(x1, x3)
U46_ga(x1, x2, x3, x4)  =  U46_ga(x1, x3, x4)
U47_ga(x1, x2, x3)  =  U47_ga(x1, x3)
U41_ga(x1, x2, x3, x4, x5)  =  U41_ga(x1, x2, x3, x5)
QSE_IN_GA(x1, x2)  =  QSE_IN_GA(x1)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x2, x4)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x4, x5)

We have to consider all (P,R,Pi)-chains

(38) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(39) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QSE_IN_GA(.(X1, X2), X3) → U7_GA(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U7_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → QSE_IN_GA(X4, X6)
U7_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U9_GA(X1, X2, X3, X5, qscE_in_ga(X4, X6))
U9_GA(X1, X2, X3, X5, qscE_out_ga(X4, X6)) → QSE_IN_GA(X5, X7)

The TRS R consists of the following rules:

partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U35_ggaa(X1, X2, X3, X4, X5, lesscA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U37_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
qscE_in_ga([], []) → qscE_out_ga([], [])
qscE_in_ga(.(X1, X2), X3) → U48_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U35_ggaa(X1, X2, X3, X4, X5, lesscA_out_gg(X1, X2)) → U36_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
U37_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U48_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U49_ga(X1, X2, X3, X5, qscE_in_ga(X4, X6))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U34_gg(X1, X2, lesscA_in_gg(X1, X2))
U36_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
U49_ga(X1, X2, X3, X5, qscE_out_ga(X4, X6)) → U50_ga(X1, X2, X3, X6, qscE_in_ga(X5, X7))
U34_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
U50_ga(X1, X2, X3, X6, qscE_out_ga(X5, X7)) → U51_ga(X1, X2, X3, appcH_in_ggga(X6, X1, X7, X3))
U51_ga(X1, X2, X3, appcH_out_ggga(X6, X1, X7, X3)) → qscE_out_ga(.(X1, X2), X3)
appcH_in_ggga([], X1, X2, .(X1, X2)) → appcH_out_ggga([], X1, X2, .(X1, X2))
appcH_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U52_ggga(X1, X2, X3, X4, X5, appcH_in_ggga(X2, X3, X4, X5))
U52_ggga(X1, X2, X3, X4, X5, appcH_out_ggga(X2, X3, X4, X5)) → appcH_out_ggga(.(X1, X2), X3, X4, .(X1, X5))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
0  =  0
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U34_gg(x1, x2, x3)  =  U34_gg(x1, x2, x3)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U35_ggaa(x1, x2, x3, x4, x5, x6)  =  U35_ggaa(x1, x2, x3, x6)
U36_ggaa(x1, x2, x3, x4, x5, x6)  =  U36_ggaa(x1, x2, x3, x6)
U37_ggaa(x1, x2, x3, x4, x5, x6)  =  U37_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qscE_in_ga(x1, x2)  =  qscE_in_ga(x1)
qscE_out_ga(x1, x2)  =  qscE_out_ga(x1, x2)
U48_ga(x1, x2, x3, x4)  =  U48_ga(x1, x2, x4)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x4, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x4, x5)
U51_ga(x1, x2, x3, x4)  =  U51_ga(x1, x2, x4)
appcH_in_ggga(x1, x2, x3, x4)  =  appcH_in_ggga(x1, x2, x3)
appcH_out_ggga(x1, x2, x3, x4)  =  appcH_out_ggga(x1, x2, x3, x4)
U52_ggga(x1, x2, x3, x4, x5, x6)  =  U52_ggga(x1, x2, x3, x4, x6)
QSE_IN_GA(x1, x2)  =  QSE_IN_GA(x1)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x2, x4)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x4, x5)

We have to consider all (P,R,Pi)-chains

(40) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QSE_IN_GA(.(X1, X2)) → U7_GA(X1, X2, partcB_in_ggaa(X1, X2))
U7_GA(X1, X2, partcB_out_ggaa(X1, X2, X4, X5)) → QSE_IN_GA(X4)
U7_GA(X1, X2, partcB_out_ggaa(X1, X2, X4, X5)) → U9_GA(X1, X2, X5, qscE_in_ga(X4))
U9_GA(X1, X2, X5, qscE_out_ga(X4, X6)) → QSE_IN_GA(X5)

The TRS R consists of the following rules:

partcB_in_ggaa(X1, .(X2, X3)) → U35_ggaa(X1, X2, X3, lesscA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3)) → U37_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
partcB_in_ggaa(X1, []) → partcB_out_ggaa(X1, [], [], [])
qscE_in_ga([]) → qscE_out_ga([], [])
qscE_in_ga(.(X1, X2)) → U48_ga(X1, X2, partcB_in_ggaa(X1, X2))
U35_ggaa(X1, X2, X3, lesscA_out_gg(X1, X2)) → U36_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U37_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U48_ga(X1, X2, partcB_out_ggaa(X1, X2, X4, X5)) → U49_ga(X1, X2, X5, qscE_in_ga(X4))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U34_gg(X1, X2, lesscA_in_gg(X1, X2))
U36_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
U49_ga(X1, X2, X5, qscE_out_ga(X4, X6)) → U50_ga(X1, X2, X6, qscE_in_ga(X5))
U34_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
U50_ga(X1, X2, X6, qscE_out_ga(X5, X7)) → U51_ga(X1, X2, appcH_in_ggga(X6, X1, X7))
U51_ga(X1, X2, appcH_out_ggga(X6, X1, X7, X3)) → qscE_out_ga(.(X1, X2), X3)
appcH_in_ggga([], X1, X2) → appcH_out_ggga([], X1, X2, .(X1, X2))
appcH_in_ggga(.(X1, X2), X3, X4) → U52_ggga(X1, X2, X3, X4, appcH_in_ggga(X2, X3, X4))
U52_ggga(X1, X2, X3, X4, appcH_out_ggga(X2, X3, X4, X5)) → appcH_out_ggga(.(X1, X2), X3, X4, .(X1, X5))

The set Q consists of the following terms:

partcB_in_ggaa(x0, x1)
qscE_in_ga(x0)
U35_ggaa(x0, x1, x2, x3)
U37_ggaa(x0, x1, x2, x3)
U48_ga(x0, x1, x2)
lesscA_in_gg(x0, x1)
U36_ggaa(x0, x1, x2, x3)
U49_ga(x0, x1, x2, x3)
U34_gg(x0, x1, x2)
U50_ga(x0, x1, x2, x3)
U51_ga(x0, x1, x2)
appcH_in_ggga(x0, x1, x2)
U52_ggga(x0, x1, x2, x3, x4)

We have to consider all (P,Q,R)-chains.

(42) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


U7_GA(X1, X2, partcB_out_ggaa(X1, X2, X4, X5)) → QSE_IN_GA(X4)
U7_GA(X1, X2, partcB_out_ggaa(X1, X2, X4, X5)) → U9_GA(X1, X2, X5, qscE_in_ga(X4))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x2   
POL(0) = 0   
POL(QSE_IN_GA(x1)) = 1 + x1   
POL(U34_gg(x1, x2, x3)) = 1   
POL(U35_ggaa(x1, x2, x3, x4)) = 1 + x3 + x4   
POL(U36_ggaa(x1, x2, x3, x4)) = 1 + x4   
POL(U37_ggaa(x1, x2, x3, x4)) = 1 + x4   
POL(U48_ga(x1, x2, x3)) = 0   
POL(U49_ga(x1, x2, x3, x4)) = 0   
POL(U50_ga(x1, x2, x3, x4)) = 0   
POL(U51_ga(x1, x2, x3)) = 0   
POL(U52_ggga(x1, x2, x3, x4, x5)) = 0   
POL(U7_GA(x1, x2, x3)) = 1 + x3   
POL(U9_GA(x1, x2, x3, x4)) = 1 + x3   
POL([]) = 0   
POL(appcH_in_ggga(x1, x2, x3)) = 0   
POL(appcH_out_ggga(x1, x2, x3, x4)) = 0   
POL(lesscA_in_gg(x1, x2)) = 1   
POL(lesscA_out_gg(x1, x2)) = 1   
POL(partcB_in_ggaa(x1, x2)) = 1 + x2   
POL(partcB_out_ggaa(x1, x2, x3, x4)) = 1 + x3 + x4   
POL(qscE_in_ga(x1)) = 0   
POL(qscE_out_ga(x1, x2)) = 0   
POL(s(x1)) = 0   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

partcB_in_ggaa(X1, .(X2, X3)) → U35_ggaa(X1, X2, X3, lesscA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3)) → U37_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
partcB_in_ggaa(X1, []) → partcB_out_ggaa(X1, [], [], [])
U35_ggaa(X1, X2, X3, lesscA_out_gg(X1, X2)) → U36_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U36_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U34_gg(X1, X2, lesscA_in_gg(X1, X2))
U37_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U34_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))

(43) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QSE_IN_GA(.(X1, X2)) → U7_GA(X1, X2, partcB_in_ggaa(X1, X2))
U9_GA(X1, X2, X5, qscE_out_ga(X4, X6)) → QSE_IN_GA(X5)

The TRS R consists of the following rules:

partcB_in_ggaa(X1, .(X2, X3)) → U35_ggaa(X1, X2, X3, lesscA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3)) → U37_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
partcB_in_ggaa(X1, []) → partcB_out_ggaa(X1, [], [], [])
qscE_in_ga([]) → qscE_out_ga([], [])
qscE_in_ga(.(X1, X2)) → U48_ga(X1, X2, partcB_in_ggaa(X1, X2))
U35_ggaa(X1, X2, X3, lesscA_out_gg(X1, X2)) → U36_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U37_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U48_ga(X1, X2, partcB_out_ggaa(X1, X2, X4, X5)) → U49_ga(X1, X2, X5, qscE_in_ga(X4))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U34_gg(X1, X2, lesscA_in_gg(X1, X2))
U36_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
U49_ga(X1, X2, X5, qscE_out_ga(X4, X6)) → U50_ga(X1, X2, X6, qscE_in_ga(X5))
U34_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
U50_ga(X1, X2, X6, qscE_out_ga(X5, X7)) → U51_ga(X1, X2, appcH_in_ggga(X6, X1, X7))
U51_ga(X1, X2, appcH_out_ggga(X6, X1, X7, X3)) → qscE_out_ga(.(X1, X2), X3)
appcH_in_ggga([], X1, X2) → appcH_out_ggga([], X1, X2, .(X1, X2))
appcH_in_ggga(.(X1, X2), X3, X4) → U52_ggga(X1, X2, X3, X4, appcH_in_ggga(X2, X3, X4))
U52_ggga(X1, X2, X3, X4, appcH_out_ggga(X2, X3, X4, X5)) → appcH_out_ggga(.(X1, X2), X3, X4, .(X1, X5))

The set Q consists of the following terms:

partcB_in_ggaa(x0, x1)
qscE_in_ga(x0)
U35_ggaa(x0, x1, x2, x3)
U37_ggaa(x0, x1, x2, x3)
U48_ga(x0, x1, x2)
lesscA_in_gg(x0, x1)
U36_ggaa(x0, x1, x2, x3)
U49_ga(x0, x1, x2, x3)
U34_gg(x0, x1, x2)
U50_ga(x0, x1, x2, x3)
U51_ga(x0, x1, x2)
appcH_in_ggga(x0, x1, x2)
U52_ggga(x0, x1, x2, x3, x4)

We have to consider all (P,Q,R)-chains.

(44) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(45) TRUE

(46) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QSC_IN_GA(.(X1, .(X2, X3)), X4) → U19_GA(X1, X2, X3, X4, lesscA_in_gg(X1, X2))
U19_GA(X1, X2, X3, X4, lesscA_out_gg(X1, X2)) → U21_GA(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U21_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → QSC_IN_GA(.(X2, X5), X7)

The TRS R consists of the following rules:

lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U34_gg(X1, X2, lesscA_in_gg(X1, X2))
U34_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U35_ggaa(X1, X2, X3, X4, X5, lesscA_in_gg(X1, X2))
U35_ggaa(X1, X2, X3, X4, X5, lesscA_out_gg(X1, X2)) → U36_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U37_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U37_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U36_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscE_in_ga([], []) → qscE_out_ga([], [])
qscE_in_ga(.(X1, X2), X3) → U48_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U48_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U49_ga(X1, X2, X3, X5, qscE_in_ga(X4, X6))
U49_ga(X1, X2, X3, X5, qscE_out_ga(X4, X6)) → U50_ga(X1, X2, X3, X6, qscE_in_ga(X5, X7))
U50_ga(X1, X2, X3, X6, qscE_out_ga(X5, X7)) → U51_ga(X1, X2, X3, appcH_in_ggga(X6, X1, X7, X3))
appcH_in_ggga([], X1, X2, .(X1, X2)) → appcH_out_ggga([], X1, X2, .(X1, X2))
appcH_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U52_ggga(X1, X2, X3, X4, X5, appcH_in_ggga(X2, X3, X4, X5))
U52_ggga(X1, X2, X3, X4, X5, appcH_out_ggga(X2, X3, X4, X5)) → appcH_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U51_ga(X1, X2, X3, appcH_out_ggga(X6, X1, X7, X3)) → qscE_out_ga(.(X1, X2), X3)
qscG_in_a([]) → qscG_out_a([])
qscC_in_ga([], []) → qscC_out_ga([], [])
qscC_in_ga(.(X1, .(X2, X3)), X4) → U38_ga(X1, X2, X3, X4, lesscA_in_gg(X1, X2))
U38_ga(X1, X2, X3, X4, lesscA_out_gg(X1, X2)) → U39_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U39_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U40_ga(X1, X2, X3, X4, X6, qscC_in_ga(.(X2, X5), X7))
qscC_in_ga(.(X1, .(X2, X3)), X4) → U42_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U42_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U43_ga(X1, X2, X3, X4, X6, qscE_in_ga(X5, X7))
U43_ga(X1, X2, X3, X4, X6, qscE_out_ga(X5, X7)) → U44_ga(X1, X2, X3, X4, qcD_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcD_in_gagga(X1, X2, X3, X4, X5) → U54_gagga(X1, X2, X3, X4, X5, qscE_in_ga(X1, X2))
U54_gagga(X1, X2, X3, X4, X5, qscE_out_ga(X1, X2)) → U55_gagga(X1, X2, X3, X4, X5, appcF_in_ggga(X3, X4, X2, X5))
appcF_in_ggga([], X1, X2, .(X1, X2)) → appcF_out_ggga([], X1, X2, .(X1, X2))
appcF_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U53_ggga(X1, X2, X3, X4, X5, appcF_in_ggga(X2, X3, X4, X5))
U53_ggga(X1, X2, X3, X4, X5, appcF_out_ggga(X2, X3, X4, X5)) → appcF_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U55_gagga(X1, X2, X3, X4, X5, appcF_out_ggga(X3, X4, X2, X5)) → qcD_out_gagga(X1, X2, X3, X4, X5)
U44_ga(X1, X2, X3, X4, qcD_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscC_out_ga(.(X1, .(X2, X3)), X4)
qscC_in_ga(.(X1, []), X2) → U45_ga(X1, X2, qscG_in_a(X3))
U45_ga(X1, X2, qscG_out_a(X3)) → U46_ga(X1, X2, X3, qscG_in_a(X4))
U46_ga(X1, X2, X3, qscG_out_a(X4)) → U47_ga(X1, X2, appcF_in_ggga(X3, X1, X4, X2))
U47_ga(X1, X2, appcF_out_ggga(X3, X1, X4, X2)) → qscC_out_ga(.(X1, []), X2)
U40_ga(X1, X2, X3, X4, X6, qscC_out_ga(.(X2, X5), X7)) → U41_ga(X1, X2, X3, X4, qcD_in_gagga(X6, X8, X7, X1, X4))
U41_ga(X1, X2, X3, X4, qcD_out_gagga(X6, X8, X7, X1, X4)) → qscC_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
0  =  0
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U34_gg(x1, x2, x3)  =  U34_gg(x1, x2, x3)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U35_ggaa(x1, x2, x3, x4, x5, x6)  =  U35_ggaa(x1, x2, x3, x6)
U36_ggaa(x1, x2, x3, x4, x5, x6)  =  U36_ggaa(x1, x2, x3, x6)
U37_ggaa(x1, x2, x3, x4, x5, x6)  =  U37_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qscE_in_ga(x1, x2)  =  qscE_in_ga(x1)
qscE_out_ga(x1, x2)  =  qscE_out_ga(x1, x2)
U48_ga(x1, x2, x3, x4)  =  U48_ga(x1, x2, x4)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x4, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x4, x5)
U51_ga(x1, x2, x3, x4)  =  U51_ga(x1, x2, x4)
appcH_in_ggga(x1, x2, x3, x4)  =  appcH_in_ggga(x1, x2, x3)
appcH_out_ggga(x1, x2, x3, x4)  =  appcH_out_ggga(x1, x2, x3, x4)
U52_ggga(x1, x2, x3, x4, x5, x6)  =  U52_ggga(x1, x2, x3, x4, x6)
qscG_in_a(x1)  =  qscG_in_a
qscG_out_a(x1)  =  qscG_out_a(x1)
qscC_in_ga(x1, x2)  =  qscC_in_ga(x1)
qscC_out_ga(x1, x2)  =  qscC_out_ga(x1, x2)
U38_ga(x1, x2, x3, x4, x5)  =  U38_ga(x1, x2, x3, x5)
U39_ga(x1, x2, x3, x4, x5)  =  U39_ga(x1, x2, x3, x5)
U40_ga(x1, x2, x3, x4, x5, x6)  =  U40_ga(x1, x2, x3, x5, x6)
U42_ga(x1, x2, x3, x4, x5)  =  U42_ga(x1, x2, x3, x5)
U43_ga(x1, x2, x3, x4, x5, x6)  =  U43_ga(x1, x2, x3, x5, x6)
U44_ga(x1, x2, x3, x4, x5)  =  U44_ga(x1, x2, x3, x5)
qcD_in_gagga(x1, x2, x3, x4, x5)  =  qcD_in_gagga(x1, x3, x4)
U54_gagga(x1, x2, x3, x4, x5, x6)  =  U54_gagga(x1, x3, x4, x6)
U55_gagga(x1, x2, x3, x4, x5, x6)  =  U55_gagga(x1, x2, x3, x4, x6)
appcF_in_ggga(x1, x2, x3, x4)  =  appcF_in_ggga(x1, x2, x3)
appcF_out_ggga(x1, x2, x3, x4)  =  appcF_out_ggga(x1, x2, x3, x4)
U53_ggga(x1, x2, x3, x4, x5, x6)  =  U53_ggga(x1, x2, x3, x4, x6)
qcD_out_gagga(x1, x2, x3, x4, x5)  =  qcD_out_gagga(x1, x2, x3, x4, x5)
U45_ga(x1, x2, x3)  =  U45_ga(x1, x3)
U46_ga(x1, x2, x3, x4)  =  U46_ga(x1, x3, x4)
U47_ga(x1, x2, x3)  =  U47_ga(x1, x3)
U41_ga(x1, x2, x3, x4, x5)  =  U41_ga(x1, x2, x3, x5)
QSC_IN_GA(x1, x2)  =  QSC_IN_GA(x1)
U19_GA(x1, x2, x3, x4, x5)  =  U19_GA(x1, x2, x3, x5)
U21_GA(x1, x2, x3, x4, x5)  =  U21_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(47) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(48) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QSC_IN_GA(.(X1, .(X2, X3)), X4) → U19_GA(X1, X2, X3, X4, lesscA_in_gg(X1, X2))
U19_GA(X1, X2, X3, X4, lesscA_out_gg(X1, X2)) → U21_GA(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U21_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → QSC_IN_GA(.(X2, X5), X7)

The TRS R consists of the following rules:

lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U34_gg(X1, X2, lesscA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U35_ggaa(X1, X2, X3, X4, X5, lesscA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U37_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U34_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
U35_ggaa(X1, X2, X3, X4, X5, lesscA_out_gg(X1, X2)) → U36_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
U37_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U36_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
0  =  0
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U34_gg(x1, x2, x3)  =  U34_gg(x1, x2, x3)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U35_ggaa(x1, x2, x3, x4, x5, x6)  =  U35_ggaa(x1, x2, x3, x6)
U36_ggaa(x1, x2, x3, x4, x5, x6)  =  U36_ggaa(x1, x2, x3, x6)
U37_ggaa(x1, x2, x3, x4, x5, x6)  =  U37_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
QSC_IN_GA(x1, x2)  =  QSC_IN_GA(x1)
U19_GA(x1, x2, x3, x4, x5)  =  U19_GA(x1, x2, x3, x5)
U21_GA(x1, x2, x3, x4, x5)  =  U21_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(49) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(50) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QSC_IN_GA(.(X1, .(X2, X3))) → U19_GA(X1, X2, X3, lesscA_in_gg(X1, X2))
U19_GA(X1, X2, X3, lesscA_out_gg(X1, X2)) → U21_GA(X1, X2, X3, partcB_in_ggaa(X1, X3))
U21_GA(X1, X2, X3, partcB_out_ggaa(X1, X3, X5, X6)) → QSC_IN_GA(.(X2, X5))

The TRS R consists of the following rules:

lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U34_gg(X1, X2, lesscA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3)) → U35_ggaa(X1, X2, X3, lesscA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3)) → U37_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
partcB_in_ggaa(X1, []) → partcB_out_ggaa(X1, [], [], [])
U34_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
U35_ggaa(X1, X2, X3, lesscA_out_gg(X1, X2)) → U36_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U37_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U36_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)

The set Q consists of the following terms:

lesscA_in_gg(x0, x1)
partcB_in_ggaa(x0, x1)
U34_gg(x0, x1, x2)
U35_ggaa(x0, x1, x2, x3)
U37_ggaa(x0, x1, x2, x3)
U36_ggaa(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(51) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


QSC_IN_GA(.(X1, .(X2, X3))) → U19_GA(X1, X2, X3, lesscA_in_gg(X1, X2))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U19_GA(x1, ..., x4) ) = 2x3 + 1


POL( U21_GA(x1, ..., x4) ) = x4 + 1


POL( U35_ggaa(x1, ..., x4) ) = 2x3 + 2


POL( lesscA_in_gg(x1, x2) ) = 0


POL( 0 ) = 1


POL( s(x1) ) = 1


POL( lesscA_out_gg(x1, x2) ) = max{0, x1 + 2x2 - 2}


POL( U34_gg(x1, ..., x3) ) = 2x1 + 2x3 + 1


POL( partcB_in_ggaa(x1, x2) ) = 2x2


POL( .(x1, x2) ) = x2 + 1


POL( U37_ggaa(x1, ..., x4) ) = x4 + 2


POL( [] ) = 0


POL( partcB_out_ggaa(x1, ..., x4) ) = max{0, 2x3 - 1}


POL( U36_ggaa(x1, ..., x4) ) = x4 + 2


POL( QSC_IN_GA(x1) ) = max{0, 2x1 - 2}



The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

partcB_in_ggaa(X1, .(X2, X3)) → U35_ggaa(X1, X2, X3, lesscA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3)) → U37_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
partcB_in_ggaa(X1, []) → partcB_out_ggaa(X1, [], [], [])
U35_ggaa(X1, X2, X3, lesscA_out_gg(X1, X2)) → U36_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U36_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
U37_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))

(52) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U19_GA(X1, X2, X3, lesscA_out_gg(X1, X2)) → U21_GA(X1, X2, X3, partcB_in_ggaa(X1, X3))
U21_GA(X1, X2, X3, partcB_out_ggaa(X1, X3, X5, X6)) → QSC_IN_GA(.(X2, X5))

The TRS R consists of the following rules:

lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U34_gg(X1, X2, lesscA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3)) → U35_ggaa(X1, X2, X3, lesscA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3)) → U37_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
partcB_in_ggaa(X1, []) → partcB_out_ggaa(X1, [], [], [])
U34_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
U35_ggaa(X1, X2, X3, lesscA_out_gg(X1, X2)) → U36_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U37_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U36_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)

The set Q consists of the following terms:

lesscA_in_gg(x0, x1)
partcB_in_ggaa(x0, x1)
U34_gg(x0, x1, x2)
U35_ggaa(x0, x1, x2, x3)
U37_ggaa(x0, x1, x2, x3)
U36_ggaa(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(53) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(54) TRUE